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 =