# HG changeset patch
# User wenzelm
# Date 1254235349 -7200
# Node ID 58e5f4ae52a6793366ee56257eecd7bd80551216
# Parent  bf8881f6e3431d2f6a151cacb441f5d59bed6cc8
Synchronized and Unsynchronized;

diff -r bf8881f6e343 -r 58e5f4ae52a6 NEWS
--- a/NEWS	Tue Sep 29 16:42:02 2009 +0200
+++ b/NEWS	Tue Sep 29 16:42:29 2009 +0200
@@ -182,6 +182,19 @@
 
 *** 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.
+
 * PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
 parallel tactical reasoning.