use Synchronized.var and prevent global CRITICAL sections in this hot spot;
authorwenzelm
Sun Aug 15 19:36:13 2010 +0200 (2010-08-15 ago)
changeset 384207bdf6c79a2db
parent 38419 f9dc924e54f8
child 38421 6cfc6fce7bfb
use Synchronized.var and prevent global CRITICAL sections in this hot spot;
src/Pure/System/isar_document.ML
     1.1 --- a/src/Pure/System/isar_document.ML	Sun Aug 15 19:30:11 2010 +0200
     1.2 +++ b/src/Pure/System/isar_document.ML	Sun Aug 15 19:36:13 2010 +0200
     1.3 @@ -7,27 +7,13 @@
     1.4  structure Isar_Document: sig end =
     1.5  struct
     1.6  
     1.7 -(* global document state *)
     1.8 -
     1.9 -local val global_state = Unsynchronized.ref Document.init_state in
    1.10 -
    1.11 -fun change_state f =
    1.12 -  NAMED_CRITICAL "Isar_Document" (fn () => Unsynchronized.change global_state f);
    1.13 -
    1.14 -fun current_state () = ! global_state;
    1.15 -
    1.16 -end;
    1.17 -
    1.18 -
    1.19 -(* define command *)
    1.20 +val global_state = Synchronized.var "Isar_Document" Document.init_state;
    1.21 +val change_state = Synchronized.change global_state;
    1.22  
    1.23  val _ =
    1.24    Isabelle_Process.add_command "Isar_Document.define_command"
    1.25      (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
    1.26  
    1.27 -
    1.28 -(* edit document version *)
    1.29 -
    1.30  val _ =
    1.31    Isabelle_Process.add_command "Isar_Document.edit_version"
    1.32      (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>