1 (* Title: Pure/System/isabelle_process.ML
4 Isabelle process wrapper, based on private fifos for maximum
5 robustness and performance.
8 . raw Posix process startup with uncontrolled output on stdout/stderr
9 . stdout \002: ML running
10 .. stdin/stdout/stderr freely available (raw ML loop)
11 .. protocol thread initialization
12 ... switch to in_fifo/out_fifo channels (rendezvous via open)
13 ... out_fifo INIT(pid): channels ready
14 ... out_fifo STATUS(keywords)
15 ... out_fifo READY: main loop ready
18 signature ISABELLE_PROCESS =
20 val isabelle_processN: string
21 val add_command: string -> (string list -> unit) -> unit
22 val command: string -> string list -> unit
23 val crashes: exn list Unsynchronized.ref
24 val init: string -> string -> unit
27 structure Isabelle_Process: ISABELLE_PROCESS =
32 val isabelle_processN = "isabelle_process";
34 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
35 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
42 val global_commands = Unsynchronized.ref (Symtab.empty: (string list -> unit) Symtab.table);
46 fun add_command name cmd = CRITICAL (fn () =>
47 Unsynchronized.change global_commands (fn cmds =>
48 (if not (Symtab.defined cmds name) then ()
49 else warning ("Redefining Isabelle process command " ^ quote name);
50 Symtab.update (name, cmd) cmds)));
52 fun command name args =
53 (case Symtab.lookup (! global_commands) name of
54 NONE => error ("Undefined Isabelle process command " ^ quote name)
55 | SOME cmd => cmd args);
64 fun chunk s = string_of_int (size s) ^ "\n" ^ s;
66 fun message _ _ _ "" = ()
67 | message out_stream ch raw_props body =
69 val robust_props = map (pairself YXML.escape_controls) raw_props;
70 val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
71 in TextIO.output (out_stream, chunk header ^ chunk body) (*atomic output!*) end;
75 fun standard_message out_stream with_serial ch body =
77 ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
78 (Position.properties_of (Position.thread_data ()))) body;
80 fun init_message out_stream =
81 message out_stream "A" [] (Session.welcome ());
90 fun auto_flush stream =
92 val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
94 (OS.Process.sleep (Time.fromMilliseconds 20); try TextIO.flushOut stream; loop ());
99 fun setup_channels in_fifo out_fifo =
102 val in_stream = TextIO.openIn in_fifo;
103 val out_stream = TextIO.openOut out_fifo;
105 val _ = Simple_Thread.fork false (auto_flush out_stream);
106 val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
107 val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
109 Output.status_fn := standard_message out_stream false "B";
110 Output.report_fn := standard_message out_stream false "C";
111 Output.writeln_fn := standard_message out_stream true "D";
112 Output.tracing_fn := standard_message out_stream true "E";
113 Output.warning_fn := standard_message out_stream true "F";
114 Output.error_fn := standard_message out_stream true "G";
115 Output.priority_fn := ! Output.writeln_fn;
116 Output.prompt_fn := ignore;
117 (in_stream, out_stream)
123 (* protocol loop -- uninterruptible *)
125 val crashes = Unsynchronized.ref ([]: exn list);
130 (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
131 warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
133 fun read_chunk stream len =
136 (case Int.fromString len of
138 | NONE => error ("Isabelle process: malformed chunk header " ^ quote len));
139 val chunk = TextIO.inputN (stream, n);
143 else error ("Isabelle process: bad chunk (" ^ string_of_int m ^ " vs. " ^ string_of_int n ^ ")")
146 fun read_command stream =
147 (case TextIO.inputLine stream of
148 NONE => raise Runtime.TERMINATE
149 | SOME line => map (read_chunk stream) (space_explode "," line));
151 fun run_command name args =
152 Runtime.debugging (command name) args
154 error ("Isabelle process command failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn);
160 (case read_command stream of
161 [] => (Output.error_msg "Isabelle process: no input"; true)
162 | name :: args => (run_command name args; true))
163 handle Runtime.TERMINATE => false
164 | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
165 in if continue then loop stream else () end;
172 fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
174 val _ = OS.Process.sleep (Time.fromMilliseconds 500); (*yield to raw ML toplevel*)
175 val _ = Output.std_output Symbol.STX;
177 val _ = quick_and_dirty := true; (* FIXME !? *)
178 val _ = Context.set_thread_data NONE;
179 val _ = Unsynchronized.change print_mode
180 (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
182 val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
183 val _ = init_message out_stream;
184 val _ = Keyword.status ();
185 val _ = Output.status (Markup.markup Markup.ready "Prover ready");
186 in loop in_stream end));