# HG changeset patch
# User wenzelm
# Date 1281893773 -7200
# Node ID 7bdf6c79a2db206a40e497c86ee1d9d666f42b3a
# Parent  f9dc924e54f81cc94c0c6b8e27dbc9e8c6e12922
use Synchronized.var and prevent global CRITICAL sections in this hot spot;

diff -r f9dc924e54f8 -r 7bdf6c79a2db src/Pure/System/isar_document.ML
--- a/src/Pure/System/isar_document.ML	Sun Aug 15 19:30:11 2010 +0200
+++ b/src/Pure/System/isar_document.ML	Sun Aug 15 19:36:13 2010 +0200
@@ -7,27 +7,13 @@
 structure Isar_Document: sig end =
 struct
 
-(* global document state *)
-
-local val global_state = Unsynchronized.ref Document.init_state in
-
-fun change_state f =
-  NAMED_CRITICAL "Isar_Document" (fn () => Unsynchronized.change global_state f);
-
-fun current_state () = ! global_state;
-
-end;
-
-
-(* define command *)
+val global_state = Synchronized.var "Isar_Document" Document.init_state;
+val change_state = Synchronized.change global_state;
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.define_command"
     (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
 
-
-(* edit document version *)
-
 val _ =
   Isabelle_Process.add_command "Isar_Document.edit_version"
     (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>