src/Pure/System/isabelle_process.ML
changeset 43684 85388f5570c4
parent 43673 29eb1cd29961
child 43746 a41f618c641d
     1.1 --- a/src/Pure/System/isabelle_process.ML	Wed Jul 06 20:14:13 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Jul 06 20:46:06 2011 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    val is_active: unit -> bool
     1.5    val add_command: string -> (string list -> unit) -> unit
     1.6    val command: string -> string list -> unit
     1.7 -  val crashes: exn list Unsynchronized.ref
     1.8 +  val crashes: exn list Synchronized.var
     1.9    val init: string -> string -> unit
    1.10  end;
    1.11  
    1.12 @@ -41,18 +41,19 @@
    1.13  
    1.14  local
    1.15  
    1.16 -val global_commands = Unsynchronized.ref (Symtab.empty: (string list -> unit) Symtab.table);
    1.17 +val commands =
    1.18 +  Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table);
    1.19  
    1.20  in
    1.21  
    1.22 -fun add_command name cmd = CRITICAL (fn () =>
    1.23 -  Unsynchronized.change global_commands (fn cmds =>
    1.24 +fun add_command name cmd =
    1.25 +  Synchronized.change commands (fn cmds =>
    1.26     (if not (Symtab.defined cmds name) then ()
    1.27      else warning ("Redefining Isabelle process command " ^ quote name);
    1.28 -    Symtab.update (name, cmd) cmds)));
    1.29 +    Symtab.update (name, cmd) cmds));
    1.30  
    1.31  fun command name args =
    1.32 -  (case Symtab.lookup (! global_commands) name of
    1.33 +  (case Symtab.lookup (Synchronized.value commands) name of
    1.34      NONE => error ("Undefined Isabelle process command " ^ quote name)
    1.35    | SOME cmd => cmd args);
    1.36  
    1.37 @@ -118,12 +119,12 @@
    1.38  
    1.39  (* protocol loop -- uninterruptible *)
    1.40  
    1.41 -val crashes = Unsynchronized.ref ([]: exn list);
    1.42 +val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
    1.43  
    1.44  local
    1.45  
    1.46  fun recover crash =
    1.47 -  (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
    1.48 +  (Synchronized.change crashes (cons crash);
    1.49      warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
    1.50  
    1.51  fun read_chunk stream len =