Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
authorwenzelm
Fri, 12 Dec 2014 14:31:57 +0100
changeset 59139 e557a9ddee5f
parent 59138 853a8cb902aa
child 59140 e7f28b330cb2
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
NEWS file | annotate | diff | comparison | revisions
src/Pure/Concurrent/synchronized.ML file | annotate | diff | comparison | revisions 
--- a/NEWS	Fri Dec 12 14:30:33 2014 +0100
+++ b/NEWS	Fri Dec 12 14:31:57 2014 +0100
@@ -235,6 +235,9 @@
 * Renamed "pairself" to "apply2", in accordance to @{apply 2}.
 INCOMPATIBILITY.
 
+* Synchronized.value (ML) is actually synchronized (as in Scala):
+subtle change of semantics with minimal potential for INCOMPATIBILITY.
+
 
 *** System ***
 
--- a/src/Pure/Concurrent/synchronized.ML	Fri Dec 12 14:30:33 2014 +0100
+++ b/src/Pure/Concurrent/synchronized.ML	Fri Dec 12 14:31:57 2014 +0100
@@ -33,7 +33,8 @@
   cond = ConditionVar.conditionVar (),
   var = Unsynchronized.ref x};
 
-fun value (Var {var, ...}) = ! var;
+fun value (Var {name, lock, var, ...}) =
+  Multithreading.synchronized name lock (fn () => ! var);
 
 
 (* synchronized access *)
isabelle