register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
tuned signature;
1 (* Title: Pure/System/isabelle_process.ML
4 Isabelle process wrapper, based on private fifos for maximum
5 robustness and performance, or local socket for maximum portability.
8 signature ISABELLE_PROCESS =
10 val is_active: unit -> bool
11 val protocol_command: string -> (string list -> unit) -> unit
12 val reset_tracing: Document_ID.exec -> unit
13 val crashes: exn list Synchronized.var
14 val init_fifos: string -> string -> unit
15 val init_socket: string -> unit
18 structure Isabelle_Process: ISABELLE_PROCESS =
23 val isabelle_processN = "isabelle_process";
25 fun is_active () = Print_Mode.print_mode_active isabelle_processN;
27 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
28 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
31 (* protocol commands *)
36 Synchronized.var "Isabelle_Process.commands"
37 (Symtab.empty: (string list -> unit) Symtab.table);
41 fun protocol_command name cmd =
42 Synchronized.change commands (fn cmds =>
43 (if not (Symtab.defined cmds name) then ()
44 else warning ("Redefining Isabelle protocol command " ^ quote name);
45 Symtab.update (name, cmd) cmds));
47 fun run_command name args =
48 (case Symtab.lookup (Synchronized.value commands) name of
49 NONE => error ("Undefined Isabelle protocol command " ^ quote name)
51 (Toplevel.debugging cmd args handle exn =>
52 error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
53 ML_Compiler.exn_message exn)));
58 (* restricted tracing messages *)
60 val tracing_messages =
61 Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
63 fun reset_tracing exec_id =
64 Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
66 fun update_tracing () =
67 (case Position.parse_id (Position.thread_data ()) of
72 Synchronized.change_result tracing_messages (fn tab =>
74 val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
75 val ok = n <= Options.default_int "editor_tracing_messages";
76 in (ok, Inttab.update (exec_id, n) tab) end);
81 val (text, promise) = Active.dialog_text ();
83 writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^
84 text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
85 val m = Markup.parse_int (Future.join promise)
86 handle Fail _ => error "Stopped";
88 Synchronized.change tracing_messages
89 (Inttab.map_default (exec_id, 0) (fn k => k - m))
96 val serial_props = Markup.serial_properties o serial;
98 fun init_channels channel =
100 val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
101 val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
103 val msg_channel = Message_Channel.make channel;
105 fun message name props body =
106 Message_Channel.send msg_channel (Message_Channel.message name props body);
108 fun standard_message props name body =
112 (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
114 Output.Internal.status_fn := standard_message [] Markup.statusN;
115 Output.Internal.report_fn := standard_message [] Markup.reportN;
116 Output.Internal.result_fn :=
117 (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
118 Output.Internal.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
119 Output.Internal.tracing_fn :=
120 (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
121 Output.Internal.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
122 Output.Internal.error_fn :=
123 (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
124 Output.Internal.protocol_message_fn := message Markup.protocolN;
125 Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn;
126 Output.Internal.prompt_fn := ignore;
127 message Markup.initN [] (Session.welcome ());
132 (* protocol loop -- uninterruptible *)
134 val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
139 (Synchronized.change crashes (cons crash);
140 warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
142 fun read_chunk channel len =
145 (case Int.fromString len of
147 | NONE => error ("Isabelle process: malformed header " ^ quote len));
148 val chunk = System_Channel.inputN channel n;
152 error ("Isabelle process: bad chunk (unexpected EOF after " ^
153 string_of_int i ^ " of " ^ string_of_int n ^ " bytes)")
157 fun read_command channel =
158 (case System_Channel.input_line channel of
159 NONE => raise Runtime.TERMINATE
160 | SOME line => map (read_chunk channel) (space_explode "," line));
162 fun worker_context e =
163 Future.worker_context "Isabelle_Process.loop" (Future.new_group NONE) e ();
169 (case read_command channel of
170 [] => (Output.error_msg "Isabelle process: no input"; true)
171 | name :: args => (worker_context (fn () => run_command name args); true))
172 handle Runtime.TERMINATE => false
173 | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
175 if continue then loop channel
176 else (Future.shutdown (); Execution.reset (); ())
185 [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN, Graph_Display.active_graphN];
186 val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
188 val init = uninterruptible (fn _ => fn rendezvous =>
190 val _ = SHA1_Samples.test ()
191 handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); reraise exn);
192 val _ = Output.physical_stderr Symbol.STX;
194 val _ = Printer.show_markup_default := true;
195 val _ = Context.set_thread_data NONE;
197 Unsynchronized.change print_mode
198 (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
200 val channel = rendezvous ();
201 val msg_channel = init_channels channel;
202 val _ = Session.init_protocol_handlers ();
203 val _ = loop channel;
204 in Message_Channel.shutdown msg_channel end);
206 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
207 fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);