# HG changeset patch
# User wenzelm
# Date 1262116787 -3600
# Node ID 88300168baf80efe5c6181ca3971b2db4ef70984
# Parent  c29264a16ad8286305201ad3e4b2c8e9f32e863e
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;

diff -r c29264a16ad8 -r 88300168baf8 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Tue Dec 29 20:30:40 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML	Tue Dec 29 20:59:47 2009 +0100
@@ -128,20 +128,19 @@
 
 local
 
-val global_states =
-  Synchronized.var "global_states" (Symtab.make [(no_id, empty_state)]);
+val global_states = Unsynchronized.ref (Symtab.make [(no_id, empty_state)]);
 
 in
 
 fun define_state (id: state_id) =
-  Synchronized.change global_states (Symtab.update_new (id, empty_state))
+  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 =
-  Synchronized.change global_states (Symtab.update (id, state));
+  Unsynchronized.change global_states (Symtab.update (id, state));
 
 fun the_state (id: state_id) =
-  (case Symtab.lookup (Synchronized.value global_states) id of
+  (case Symtab.lookup (! global_states) id of
     NONE => err_undef "state" id
   | SOME state => state);
 
@@ -152,17 +151,17 @@
 
 local
 
-val global_commands =
-  Synchronized.var "global_commands" (Symtab.make [(no_id, Toplevel.empty)]);
+val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]);
 
 in
 
 fun define_command id tr =
-  Synchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
-    handle Symtab.DUP dup => err_dup "command" dup;
+  NAMED_CRITICAL "Isar" (fn () =>
+    Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
+      handle Symtab.DUP dup => err_dup "command" dup);
 
 fun the_command (id: command_id) =
-  (case Symtab.lookup (Synchronized.value global_commands) id of
+  (case Symtab.lookup (! global_commands) id of
     NONE => err_undef "command" id
   | SOME tr => tr);
 
@@ -173,17 +172,17 @@
 
 local
 
-val global_documents =
-  Synchronized.var "global_documents" (Symtab.empty: document Symtab.table);
+val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
 
 in
 
 fun define_document (id: document_id) document =
-  Synchronized.change global_documents (Symtab.update_new (id, document))
-    handle Symtab.DUP dup => err_dup "document" dup;
+  NAMED_CRITICAL "Isar" (fn () =>
+    Unsynchronized.change global_documents (Symtab.update_new (id, document))
+      handle Symtab.DUP dup => err_dup "document" dup);
 
 fun the_document (id: document_id) =
-  (case Symtab.lookup (Synchronized.value global_documents) id of
+  (case Symtab.lookup (! global_documents) id of
     NONE => err_undef "document" id
   | SOME document => document);
 
@@ -204,20 +203,21 @@
   in () end;
 
 fun end_document (id: document_id) =
-  let
-    val document as Document {name, ...} = the_document id;
-    val end_state =
-      the_state (the (#state (#3 (the
-        (first_entry (fn (_, {next, ...}) => is_none next) document)))));
-    val _ =
-      Future.fork_deps [end_state] (fn () =>
-        (case Future.join end_state of
-          SOME st =>
-           (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
-            ThyInfo.touch_child_thys name;
-            ThyInfo.register_thy name)
-        | NONE => error ("Failed to finish theory " ^ quote name)));
-  in () end;
+  NAMED_CRITICAL "Isar" (fn () =>
+    let
+      val document as Document {name, ...} = the_document id;
+      val end_state =
+        the_state (the (#state (#3 (the
+          (first_entry (fn (_, {next, ...}) => is_none next) document)))));
+      val _ =
+        Future.fork_deps [end_state] (fn () =>
+          (case Future.join end_state of
+            SOME st =>
+             (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
+              ThyInfo.touch_child_thys name;
+              ThyInfo.register_thy name)
+          | NONE => error ("Failed to finish theory " ^ quote name)));
+    in () end);
 
 
 (* document editing *)
@@ -254,33 +254,34 @@
 in
 
 fun edit_document (old_id: document_id) (new_id: document_id) edits =
-  let
-    val old_document as Document {name, entries = old_entries, ...} = the_document old_id;
-    val new_document as Document {entries = new_entries, ...} = old_document
-      |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
+  NAMED_CRITICAL "Isar" (fn () =>
+    let
+      val old_document as Document {name, entries = old_entries, ...} = the_document old_id;
+      val new_document as Document {entries = new_entries, ...} = old_document
+        |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
 
-    fun cancel_old id = fold_entries id
-      (fn (_, {state = SOME state_id, ...}) => K (Future.cancel (the_state state_id)) | _ => K ())
-      old_document ();
+      fun cancel_old id = fold_entries id
+        (fn (_, {state = SOME state_id, ...}) => K (Future.cancel (the_state state_id)) | _ => K ())
+        old_document ();
 
-    val (updates, new_document') =
-      (case first_entry (is_changed old_entries) new_document of
-        NONE =>
-          (case first_entry (is_changed new_entries) old_document of
-            NONE => ([], new_document)
-          | SOME (_, id, _) => (cancel_old id; ([], new_document)))
-      | SOME (prev, id, _) =>
-          let
-            val _ = cancel_old id;
-            val prev_state_id = the (#state (the_entry new_entries (the prev)));
-            val (_, updates) = fold_entries id (new_state name) new_document (prev_state_id, []);
-            val new_document' = new_document |> map_entries (fold (set_entry_state o #1) updates);
-          in (rev updates, new_document') end);
+      val (updates, new_document') =
+        (case first_entry (is_changed old_entries) new_document of
+          NONE =>
+            (case first_entry (is_changed new_entries) old_document of
+              NONE => ([], new_document)
+            | SOME (_, id, _) => (cancel_old id; ([], new_document)))
+        | SOME (prev, id, _) =>
+            let
+              val _ = cancel_old id;
+              val prev_state_id = the (#state (the_entry new_entries (the prev)));
+              val (_, updates) = fold_entries id (new_state name) new_document (prev_state_id, []);
+              val new_document' = new_document |> map_entries (fold (set_entry_state o #1) updates);
+            in (rev updates, new_document') end);
 
-    val _ = define_document new_id new_document';
-    val _ = report_updates new_id (map #1 updates);
-    val _ = List.app (fn (_, run) => run ()) updates;
-  in () end;
+      val _ = define_document new_id new_document';
+      val _ = report_updates new_id (map #1 updates);
+      val _ = List.app (fn (_, run) => run ()) updates;
+    in () end);
 
 end;