src/Pure/System/isar.ML
changeset 32738 15bb09ca0378
parent 32486 67972a7f85b7
child 32739 31e75ad9ae17
     1.1 --- a/src/Pure/System/isar.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/System/isar.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val undo: int -> unit
     1.5    val kill: unit -> unit
     1.6    val kill_proof: unit -> unit
     1.7 -  val crashes: exn list ref
     1.8 +  val crashes: exn list Unsynchronized.ref
     1.9    val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
    1.10    val loop: unit -> unit
    1.11    val main: unit -> unit
    1.12 @@ -36,9 +36,9 @@
    1.13    (*previous state, state transition -- regular commands only*)
    1.14  
    1.15  local
    1.16 -  val global_history = ref ([]: history);
    1.17 -  val global_state = ref Toplevel.toplevel;
    1.18 -  val global_exn = ref (NONE: (exn * string) option);
    1.19 +  val global_history = Unsynchronized.ref ([]: history);
    1.20 +  val global_state = Unsynchronized.ref Toplevel.toplevel;
    1.21 +  val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
    1.22  in
    1.23  
    1.24  fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
    1.25 @@ -115,7 +115,7 @@
    1.26  
    1.27  (* toplevel loop *)
    1.28  
    1.29 -val crashes = ref ([]: exn list);
    1.30 +val crashes = Unsynchronized.ref ([]: exn list);
    1.31  
    1.32  local
    1.33  
    1.34 @@ -130,7 +130,7 @@
    1.35      handle exn =>
    1.36        (Output.error_msg (ML_Compiler.exn_message exn)
    1.37          handle crash =>
    1.38 -          (CRITICAL (fn () => change crashes (cons crash));
    1.39 +          (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
    1.40              warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
    1.41            raw_loop secure src)
    1.42    end;