src/Pure/System/isar.ML

   val >>> : Toplevel.transition list -> unit
   val linear_undo: int -> unit
   val undo: int -> unit
   val kill: unit -> unit
   val kill_proof: unit -> unit
-  val crashes: exn list ref
+  val crashes: exn list Unsynchronized.ref
   val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
   val loop: unit -> unit
   val main: unit -> unit
 end;
 

 
 type history = (Toplevel.state * Toplevel.transition) list;
   (*previous state, state transition -- regular commands only*)
 
 local
-  val global_history = ref ([]: history);
-  val global_state = ref Toplevel.toplevel;
-  val global_exn = ref (NONE: (exn * string) option);
+  val global_history = Unsynchronized.ref ([]: history);
+  val global_state = Unsynchronized.ref Toplevel.toplevel;
+  val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
 in
 
 fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
   let
     fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)

   | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
 
 
 (* toplevel loop *)
 
-val crashes = ref ([]: exn list);
+val crashes = Unsynchronized.ref ([]: exn list);
 
 local
 
 fun raw_loop secure src =
   let

       NONE => if secure then quit () else ()
     | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
     handle exn =>
       (Output.error_msg (ML_Compiler.exn_message exn)
         handle crash =>
-          (CRITICAL (fn () => change crashes (cons crash));
+          (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
             warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
           raw_loop secure src)
   end;
 
 in