src/Pure/Isar/isar_document.ML
changeset 32738 15bb09ca0378
parent 32573 62b5b538408d
child 32793 24ba50c14ec5
     1.1 --- a/src/Pure/Isar/isar_document.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Isar/isar_document.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -112,18 +112,18 @@
     1.4  (** global configuration **)
     1.5  
     1.6  local
     1.7 -  val global_states = ref (Symtab.empty: Toplevel.state option future Symtab.table);
     1.8 -  val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table);
     1.9 -  val global_documents = ref (Symtab.empty: document Symtab.table);
    1.10 +  val global_states = Unsynchronized.ref (Symtab.empty: Toplevel.state option future Symtab.table);
    1.11 +  val global_commands = Unsynchronized.ref (Symtab.empty: Toplevel.transition Symtab.table);
    1.12 +  val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
    1.13  in
    1.14  
    1.15 -fun change_states f = NAMED_CRITICAL "Isar" (fn () => change global_states f);
    1.16 +fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f);
    1.17  fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
    1.18  
    1.19 -fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f);
    1.20 +fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f);
    1.21  fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
    1.22  
    1.23 -fun change_documents f = NAMED_CRITICAL "Isar" (fn () => change global_documents f);
    1.24 +fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f);
    1.25  fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
    1.26  
    1.27  fun init () = NAMED_CRITICAL "Isar" (fn () =>