--- 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;