1.1 --- a/src/Pure/System/isar.ML	Wed Jul 06 20:14:13 2011 +0200
     1.2 +++ b/src/Pure/System/isar.ML	Wed Jul 06 20:46:06 2011 +0200
     1.3 @@ -17,7 +17,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 Unsynchronized.ref
     1.8 +  val crashes: exn list Synchronized.var
     1.9    val toplevel_loop: TextIO.instream ->
    1.10      {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
    1.11    val loop: unit -> unit
    1.12 @@ -113,7 +113,7 @@
    1.13  
    1.14  (* toplevel loop -- uninterruptible *)
    1.15  
    1.16 -val crashes = Unsynchronized.ref ([]: exn list);
    1.17 +val crashes = Synchronized.var "Isar.crashes" ([]: exn list);
    1.18  
    1.19  local
    1.20  
    1.21 @@ -128,7 +128,7 @@
    1.22      handle exn =>
    1.23        (Output.error_msg (ML_Compiler.exn_message exn)
    1.24          handle crash =>
    1.25 -          (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
    1.26 +          (Synchronized.change crashes (cons crash);
    1.27              warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
    1.28          raw_loop secure src)
    1.29    end;