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.
further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;
authorwenzelm
Thu, 27 May 2010 20:15:36 +0200
changeset 37147 0c0ef115c7aa
parent 37146 f652333bbf8e
child 37148 d515609c88f7
further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;
src/Pure/Isar/isar_document.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_document.ML	Thu May 27 18:10:37 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Thu May 27 20:15:36 2010 +0200
@@ -120,11 +120,13 @@
 in
 
 fun define_state (id: state_id) =
-  Unsynchronized.change global_states (Symtab.update_new (id, empty_state))
-    handle Symtab.DUP dup => err_dup "state" dup;
+  NAMED_CRITICAL "Isar" (fn () =>
+    Unsynchronized.change global_states (Symtab.update_new (id, empty_state))
+      handle Symtab.DUP dup => err_dup "state" dup);
 
 fun put_state (id: state_id) state =
-  Unsynchronized.change global_states (Symtab.update (id, state));
+  NAMED_CRITICAL "Isar" (fn () =>
+    Unsynchronized.change global_states (Symtab.update (id, state)));
 
 fun the_state (id: state_id) =
   (case Symtab.lookup (! global_states) id of
isabelle