Isabelle_Process: do not enforce future_terminal_proof by default -- no error propagation yet;
1 (* Title: Pure/System/isabelle_process.ML
4 Isabelle process wrapper.
6 General format of process output:
7 (1) message = "\002" header chunk body chunk
8 (2) chunk = size (ASCII digits) \n content (YXML)
11 signature ISABELLE_PROCESS =
13 val isabelle_processN: string
14 val init: string -> unit
17 structure Isabelle_Process: ISABELLE_PROCESS =
22 val isabelle_processN = "isabelle_process";
24 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
25 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
32 fun chunk s = string_of_int (size s) ^ "\n" ^ s;
34 fun message _ _ _ "" = ()
35 | message out_stream ch props body =
37 val header = YXML.string_of (XML.Elem (ch, map (pairself YXML.binary_text) props, []));
38 val msg = Symbol.STX ^ chunk header ^ chunk body;
39 in TextIO.output (out_stream, msg) (*atomic output*) end;
43 fun standard_message out_stream ch body =
44 message out_stream ch (Position.properties_of (Position.thread_data ())) body;
46 fun init_message out_stream =
47 message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
56 fun auto_flush stream =
58 val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
60 (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
65 fun setup_channels out =
67 val path = File.platform_path (Path.explode out);
68 val out_stream = TextIO.openOut path; (*fifo blocks until reader is ready*)
69 val _ = OS.FileSys.remove path; (*prevent alien access, indicate writer is ready*)
70 val _ = SimpleThread.fork false (auto_flush out_stream);
71 val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
72 val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
74 Output.status_fn := standard_message out_stream "B";
75 Output.writeln_fn := standard_message out_stream "C";
76 Output.tracing_fn := standard_message out_stream "D";
77 Output.warning_fn := standard_message out_stream "E";
78 Output.error_fn := standard_message out_stream "F";
79 Output.debug_fn := standard_message out_stream "G";
80 Output.priority_fn := ! Output.writeln_fn;
81 Output.prompt_fn := ignore;
91 (Unsynchronized.change print_mode
92 (fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]);
93 setup_channels out |> init_message;
95 Output.status (Markup.markup Markup.ready "");
96 Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});