# HG changeset patch
# User wenzelm
# Date 1274984136 -7200
# Node ID 0c0ef115c7aaf37cffdc8b5a4ad0b70f0f94cb49
# Parent  f652333bbf8ecb40143bda6329efd92446492b8c
further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;

diff -r f652333bbf8e -r 0c0ef115c7aa src/Pure/Isar/isar_document.ML
--- 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