makarius at sketis.net
Tue Sep 29 17:59:26 CEST 2009
*** ML ***
* Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
provides a high-level programming interface to synchronized state
variables with atomic update. This works via pure function
application within a critical section -- its runtime should be as
short as possible; beware of deadlocks if critical code is nested,
either directly or indirectly via other synchronized variables!
* Structure Unsynchronized (cf. src/Pure/ML-Systems/unsynchronized.ML)
wraps raw ML references, explicitly indicating their non-thread-safe
behaviour. The Isar toplevel keeps this structure open, to
accommodate Proof General as well as quick and dirty interactive
experiments with references.
More information about the isabelle-dev