equal
deleted
inserted
replaced
18 signature ISABELLE_PROCESS = |
18 signature ISABELLE_PROCESS = |
19 sig |
19 sig |
20 val is_active: unit -> bool |
20 val is_active: unit -> bool |
21 val add_command: string -> (string list -> unit) -> unit |
21 val add_command: string -> (string list -> unit) -> unit |
22 val command: string -> string list -> unit |
22 val command: string -> string list -> unit |
23 val crashes: exn list Unsynchronized.ref |
23 val crashes: exn list Synchronized.var |
24 val init: string -> string -> unit |
24 val init: string -> string -> unit |
25 end; |
25 end; |
26 |
26 |
27 structure Isabelle_Process: ISABELLE_PROCESS = |
27 structure Isabelle_Process: ISABELLE_PROCESS = |
28 struct |
28 struct |
39 |
39 |
40 (* commands *) |
40 (* commands *) |
41 |
41 |
42 local |
42 local |
43 |
43 |
44 val global_commands = Unsynchronized.ref (Symtab.empty: (string list -> unit) Symtab.table); |
44 val commands = |
|
45 Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table); |
45 |
46 |
46 in |
47 in |
47 |
48 |
48 fun add_command name cmd = CRITICAL (fn () => |
49 fun add_command name cmd = |
49 Unsynchronized.change global_commands (fn cmds => |
50 Synchronized.change commands (fn cmds => |
50 (if not (Symtab.defined cmds name) then () |
51 (if not (Symtab.defined cmds name) then () |
51 else warning ("Redefining Isabelle process command " ^ quote name); |
52 else warning ("Redefining Isabelle process command " ^ quote name); |
52 Symtab.update (name, cmd) cmds))); |
53 Symtab.update (name, cmd) cmds)); |
53 |
54 |
54 fun command name args = |
55 fun command name args = |
55 (case Symtab.lookup (! global_commands) name of |
56 (case Symtab.lookup (Synchronized.value commands) name of |
56 NONE => error ("Undefined Isabelle process command " ^ quote name) |
57 NONE => error ("Undefined Isabelle process command " ^ quote name) |
57 | SOME cmd => cmd args); |
58 | SOME cmd => cmd args); |
58 |
59 |
59 end; |
60 end; |
60 |
61 |
116 end; |
117 end; |
117 |
118 |
118 |
119 |
119 (* protocol loop -- uninterruptible *) |
120 (* protocol loop -- uninterruptible *) |
120 |
121 |
121 val crashes = Unsynchronized.ref ([]: exn list); |
122 val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); |
122 |
123 |
123 local |
124 local |
124 |
125 |
125 fun recover crash = |
126 fun recover crash = |
126 (CRITICAL (fn () => Unsynchronized.change crashes (cons crash)); |
127 (Synchronized.change crashes (cons crash); |
127 warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes"); |
128 warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes"); |
128 |
129 |
129 fun read_chunk stream len = |
130 fun read_chunk stream len = |
130 let |
131 let |
131 val n = |
132 val n = |