wenzelm@30174
|
1 |
(* Title: Pure/System/isabelle_process.ML
|
wenzelm@25528
|
2 |
Author: Makarius
|
wenzelm@25528
|
3 |
|
wenzelm@38691
|
4 |
Isabelle process wrapper, based on private fifos for maximum
|
wenzelm@49727
|
5 |
robustness and performance, or local socket for maximum portability.
|
wenzelm@25528
|
6 |
*)
|
wenzelm@25528
|
7 |
|
wenzelm@25528
|
8 |
signature ISABELLE_PROCESS =
|
wenzelm@25528
|
9 |
sig
|
wenzelm@43772
|
10 |
val is_active: unit -> bool
|
wenzelm@46990
|
11 |
val protocol_command: string -> (string list -> unit) -> unit
|
wenzelm@53792
|
12 |
val reset_tracing: Document_ID.exec -> unit
|
wenzelm@44563
|
13 |
val crashes: exn list Synchronized.var
|
wenzelm@45921
|
14 |
val init_fifos: string -> string -> unit
|
wenzelm@45920
|
15 |
val init_socket: string -> unit
|
wenzelm@25528
|
16 |
end;
|
wenzelm@25528
|
17 |
|
wenzelm@31800
|
18 |
structure Isabelle_Process: ISABELLE_PROCESS =
|
wenzelm@25528
|
19 |
struct
|
wenzelm@25528
|
20 |
|
wenzelm@43772
|
21 |
(* print mode *)
|
wenzelm@25554
|
22 |
|
wenzelm@25748
|
23 |
val isabelle_processN = "isabelle_process";
|
wenzelm@25748
|
24 |
|
wenzelm@43772
|
25 |
fun is_active () = Print_Mode.print_mode_active isabelle_processN;
|
wenzelm@43772
|
26 |
|
wenzelm@26550
|
27 |
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
|
wenzelm@28036
|
28 |
val _ = Markup.add_mode isabelle_processN YXML.output_markup;
|
wenzelm@25841
|
29 |
|
wenzelm@25841
|
30 |
|
wenzelm@46990
|
31 |
(* protocol commands *)
|
wenzelm@38568
|
32 |
|
wenzelm@38568
|
33 |
local
|
wenzelm@38568
|
34 |
|
wenzelm@44563
|
35 |
val commands =
|
wenzelm@53937
|
36 |
Synchronized.var "Isabelle_Process.commands"
|
wenzelm@53937
|
37 |
(Symtab.empty: (string list -> unit) Symtab.table);
|
wenzelm@38568
|
38 |
|
wenzelm@38568
|
39 |
in
|
wenzelm@38568
|
40 |
|
wenzelm@46990
|
41 |
fun protocol_command name cmd =
|
wenzelm@44563
|
42 |
Synchronized.change commands (fn cmds =>
|
wenzelm@38568
|
43 |
(if not (Symtab.defined cmds name) then ()
|
wenzelm@53719
|
44 |
else warning ("Redefining Isabelle protocol command " ^ quote name);
|
wenzelm@44563
|
45 |
Symtab.update (name, cmd) cmds));
|
wenzelm@38568
|
46 |
|
wenzelm@46990
|
47 |
fun run_command name args =
|
wenzelm@44563
|
48 |
(case Symtab.lookup (Synchronized.value commands) name of
|
wenzelm@53719
|
49 |
NONE => error ("Undefined Isabelle protocol command " ^ quote name)
|
wenzelm@46990
|
50 |
| SOME cmd =>
|
wenzelm@54846
|
51 |
(Toplevel.debugging cmd args handle exn =>
|
wenzelm@53719
|
52 |
error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
|
wenzelm@49071
|
53 |
ML_Compiler.exn_message exn)));
|
wenzelm@38568
|
54 |
|
wenzelm@38568
|
55 |
end;
|
wenzelm@38568
|
56 |
|
wenzelm@38568
|
57 |
|
wenzelm@51520
|
58 |
(* restricted tracing messages *)
|
wenzelm@50662
|
59 |
|
wenzelm@53242
|
60 |
val tracing_messages =
|
wenzelm@53242
|
61 |
Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
|
wenzelm@50662
|
62 |
|
wenzelm@53792
|
63 |
fun reset_tracing exec_id =
|
wenzelm@53792
|
64 |
Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
|
wenzelm@50662
|
65 |
|
wenzelm@51520
|
66 |
fun update_tracing () =
|
wenzelm@51926
|
67 |
(case Position.parse_id (Position.thread_data ()) of
|
wenzelm@50662
|
68 |
NONE => ()
|
wenzelm@53792
|
69 |
| SOME exec_id =>
|
wenzelm@51520
|
70 |
let
|
wenzelm@53697
|
71 |
val ok =
|
wenzelm@53242
|
72 |
Synchronized.change_result tracing_messages (fn tab =>
|
wenzelm@51520
|
73 |
let
|
wenzelm@53792
|
74 |
val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
|
wenzelm@53242
|
75 |
val ok = n <= Options.default_int "editor_tracing_messages";
|
wenzelm@53792
|
76 |
in (ok, Inttab.update (exec_id, n) tab) end);
|
wenzelm@51520
|
77 |
in
|
wenzelm@51520
|
78 |
if ok then ()
|
wenzelm@51520
|
79 |
else
|
wenzelm@51520
|
80 |
let
|
wenzelm@51520
|
81 |
val (text, promise) = Active.dialog_text ();
|
wenzelm@51520
|
82 |
val _ =
|
wenzelm@51520
|
83 |
writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^
|
wenzelm@52012
|
84 |
text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
|
wenzelm@51520
|
85 |
val m = Markup.parse_int (Future.join promise)
|
wenzelm@51520
|
86 |
handle Fail _ => error "Stopped";
|
wenzelm@51520
|
87 |
in
|
wenzelm@53242
|
88 |
Synchronized.change tracing_messages
|
wenzelm@53792
|
89 |
(Inttab.map_default (exec_id, 0) (fn k => k - m))
|
wenzelm@51520
|
90 |
end
|
wenzelm@51520
|
91 |
end);
|
wenzelm@50662
|
92 |
|
wenzelm@50662
|
93 |
|
wenzelm@53937
|
94 |
(* output channels *)
|
wenzelm@28188
|
95 |
|
wenzelm@53991
|
96 |
val serial_props = Markup.serial_properties o serial;
|
wenzelm@53991
|
97 |
|
wenzelm@49727
|
98 |
fun init_channels channel =
|
wenzelm@28189
|
99 |
let
|
wenzelm@40394
|
100 |
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
|
wenzelm@40394
|
101 |
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
|
wenzelm@40394
|
102 |
|
wenzelm@53721
|
103 |
val msg_channel = Message_Channel.make channel;
|
wenzelm@53717
|
104 |
|
wenzelm@53937
|
105 |
fun message name props body =
|
wenzelm@53937
|
106 |
Message_Channel.send msg_channel (Message_Channel.message name props body);
|
wenzelm@53937
|
107 |
|
wenzelm@53991
|
108 |
fun standard_message props name body =
|
wenzelm@53717
|
109 |
if body = "" then ()
|
wenzelm@53717
|
110 |
else
|
wenzelm@53937
|
111 |
message name
|
wenzelm@53991
|
112 |
(fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
|
wenzelm@28044
|
113 |
in
|
wenzelm@53991
|
114 |
Output.Internal.status_fn := standard_message [] Markup.statusN;
|
wenzelm@53991
|
115 |
Output.Internal.report_fn := standard_message [] Markup.reportN;
|
wenzelm@53991
|
116 |
Output.Internal.result_fn :=
|
wenzelm@53991
|
117 |
(fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
|
wenzelm@53991
|
118 |
Output.Internal.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
|
wenzelm@53989
|
119 |
Output.Internal.tracing_fn :=
|
wenzelm@53991
|
120 |
(fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
|
wenzelm@53991
|
121 |
Output.Internal.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
|
wenzelm@55760
|
122 |
Output.Internal.error_message_fn :=
|
wenzelm@53991
|
123 |
(fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
|
wenzelm@53989
|
124 |
Output.Internal.protocol_message_fn := message Markup.protocolN;
|
wenzelm@53989
|
125 |
Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn;
|
wenzelm@53989
|
126 |
Output.Internal.prompt_fn := ignore;
|
wenzelm@53937
|
127 |
message Markup.initN [] (Session.welcome ());
|
wenzelm@53721
|
128 |
msg_channel
|
wenzelm@28044
|
129 |
end;
|
wenzelm@25841
|
130 |
|
wenzelm@25841
|
131 |
|
wenzelm@39511
|
132 |
(* protocol loop -- uninterruptible *)
|
wenzelm@38568
|
133 |
|
wenzelm@44563
|
134 |
val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
|
wenzelm@38568
|
135 |
|
wenzelm@38568
|
136 |
local
|
wenzelm@38568
|
137 |
|
wenzelm@38568
|
138 |
fun recover crash =
|
wenzelm@44563
|
139 |
(Synchronized.change crashes (cons crash);
|
wenzelm@38568
|
140 |
warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
|
wenzelm@38568
|
141 |
|
wenzelm@45921
|
142 |
fun read_chunk channel len =
|
wenzelm@38568
|
143 |
let
|
wenzelm@38568
|
144 |
val n =
|
wenzelm@38568
|
145 |
(case Int.fromString len of
|
wenzelm@38568
|
146 |
SOME n => n
|
wenzelm@53936
|
147 |
| NONE => error ("Isabelle process: malformed header " ^ quote len));
|
wenzelm@45921
|
148 |
val chunk = System_Channel.inputN channel n;
|
wenzelm@53936
|
149 |
val i = size chunk;
|
wenzelm@38568
|
150 |
in
|
wenzelm@53936
|
151 |
if i <> n then
|
wenzelm@53936
|
152 |
error ("Isabelle process: bad chunk (unexpected EOF after " ^
|
wenzelm@53936
|
153 |
string_of_int i ^ " of " ^ string_of_int n ^ " bytes)")
|
wenzelm@53936
|
154 |
else chunk
|
wenzelm@38568
|
155 |
end;
|
wenzelm@38568
|
156 |
|
wenzelm@45921
|
157 |
fun read_command channel =
|
wenzelm@45921
|
158 |
(case System_Channel.input_line channel of
|
wenzelm@38568
|
159 |
NONE => raise Runtime.TERMINATE
|
wenzelm@45921
|
160 |
| SOME line => map (read_chunk channel) (space_explode "," line));
|
wenzelm@38568
|
161 |
|
wenzelm@55298
|
162 |
fun task_context e =
|
wenzelm@55298
|
163 |
Future.task_context "Isabelle_Process.loop" (Future.new_group NONE) e ();
|
wenzelm@53696
|
164 |
|
wenzelm@38568
|
165 |
in
|
wenzelm@38568
|
166 |
|
wenzelm@45921
|
167 |
fun loop channel =
|
wenzelm@38568
|
168 |
let val continue =
|
wenzelm@45921
|
169 |
(case read_command channel of
|
wenzelm@55760
|
170 |
[] => (Output.error_message "Isabelle process: no input"; true)
|
wenzelm@55298
|
171 |
| name :: args => (task_context (fn () => run_command name args); true))
|
wenzelm@38568
|
172 |
handle Runtime.TERMINATE => false
|
wenzelm@55760
|
173 |
| exn => (ML_Compiler.exn_error_message exn handle crash => recover crash; true);
|
wenzelm@53907
|
174 |
in
|
wenzelm@53907
|
175 |
if continue then loop channel
|
wenzelm@54329
|
176 |
else (Future.shutdown (); Execution.reset (); ())
|
wenzelm@53907
|
177 |
end;
|
wenzelm@38568
|
178 |
|
wenzelm@38568
|
179 |
end;
|
wenzelm@38568
|
180 |
|
wenzelm@38568
|
181 |
|
wenzelm@25554
|
182 |
(* init *)
|
wenzelm@25554
|
183 |
|
wenzelm@51730
|
184 |
val default_modes1 =
|
wenzelm@51730
|
185 |
[Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN, Graph_Display.active_graphN];
|
wenzelm@51730
|
186 |
val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
|
wenzelm@50581
|
187 |
|
wenzelm@53715
|
188 |
val init = uninterruptible (fn _ => fn rendezvous =>
|
wenzelm@38551
|
189 |
let
|
wenzelm@54349
|
190 |
val _ = SHA1_Samples.test ()
|
wenzelm@54349
|
191 |
handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); reraise exn);
|
wenzelm@47430
|
192 |
val _ = Output.physical_stderr Symbol.STX;
|
wenzelm@39797
|
193 |
|
wenzelm@50676
|
194 |
val _ = Printer.show_markup_default := true;
|
wenzelm@39797
|
195 |
val _ = Context.set_thread_data NONE;
|
wenzelm@44546
|
196 |
val _ =
|
wenzelm@44546
|
197 |
Unsynchronized.change print_mode
|
wenzelm@50581
|
198 |
(fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
|
wenzelm@39797
|
199 |
|
wenzelm@45921
|
200 |
val channel = rendezvous ();
|
wenzelm@53721
|
201 |
val msg_channel = init_channels channel;
|
wenzelm@53248
|
202 |
val _ = Session.init_protocol_handlers ();
|
wenzelm@53720
|
203 |
val _ = loop channel;
|
wenzelm@53721
|
204 |
in Message_Channel.shutdown msg_channel end);
|
wenzelm@25528
|
205 |
|
wenzelm@45921
|
206 |
fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
|
wenzelm@45921
|
207 |
fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);
|
wenzelm@45920
|
208 |
|
wenzelm@25528
|
209 |
end;
|
wenzelm@39797
|
210 |
|