On 04/12/16 11:14, Lars Hupel wrote: >> Where did you see these lots of Unsynchronized.ref (or better >> Synchronized.var) in Isabelle Tools? > > There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools", 181 > in "~~/src/HOL", and some more in the AFP (many of which appear to be in > generated code).
So what is wrong here? Tending global state (normally via Synchronized.var and not the raw Unsynchronized.ref) has been part of the normal routine of Isabelle maintenance in the last 10 years. At the beginning almost nothing worked, but around 2008/2009 it became routine. Today we have a fairly robust system, with lots of user tools that are mostly thread-safe. The "implementation" manual (sections 0.7.9 and 0.8) has some brief explanations for users of Isabelle/ML. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev