wenzelm@30174
|
1 |
(* Title: Pure/System/isabelle_process.ML
|
wenzelm@25528
|
2 |
Author: Makarius
|
wenzelm@25528
|
3 |
|
wenzelm@34102
|
4 |
Isabelle process wrapper.
|
wenzelm@25631
|
5 |
|
wenzelm@25631
|
6 |
General format of process output:
|
wenzelm@34102
|
7 |
(1) message = "\002" header chunk body chunk
|
wenzelm@34102
|
8 |
(2) chunk = size (ASCII digits) \n content (YXML)
|
wenzelm@25528
|
9 |
*)
|
wenzelm@25528
|
10 |
|
wenzelm@25528
|
11 |
signature ISABELLE_PROCESS =
|
wenzelm@25528
|
12 |
sig
|
wenzelm@26574
|
13 |
val isabelle_processN: string
|
wenzelm@28044
|
14 |
val init: string -> unit
|
wenzelm@25528
|
15 |
end;
|
wenzelm@25528
|
16 |
|
wenzelm@31800
|
17 |
structure Isabelle_Process: ISABELLE_PROCESS =
|
wenzelm@25528
|
18 |
struct
|
wenzelm@25528
|
19 |
|
wenzelm@26550
|
20 |
(* print modes *)
|
wenzelm@25554
|
21 |
|
wenzelm@25748
|
22 |
val isabelle_processN = "isabelle_process";
|
wenzelm@25748
|
23 |
|
wenzelm@26550
|
24 |
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
|
wenzelm@28036
|
25 |
val _ = Markup.add_mode isabelle_processN YXML.output_markup;
|
wenzelm@25841
|
26 |
|
wenzelm@25841
|
27 |
|
wenzelm@25841
|
28 |
(* message markup *)
|
wenzelm@25841
|
29 |
|
wenzelm@25841
|
30 |
local
|
wenzelm@25810
|
31 |
|
wenzelm@34102
|
32 |
fun chunk s = string_of_int (size s) ^ "\n" ^ s;
|
wenzelm@26574
|
33 |
|
wenzelm@34102
|
34 |
fun message _ _ _ "" = ()
|
wenzelm@34102
|
35 |
| message out_stream ch props body =
|
wenzelm@34102
|
36 |
let
|
wenzelm@34102
|
37 |
val header = YXML.string_of (XML.Elem (ch, map (pairself YXML.binary_text) props, []));
|
wenzelm@34102
|
38 |
val msg = Symbol.STX ^ chunk header ^ chunk body;
|
wenzelm@34102
|
39 |
in TextIO.output (out_stream, msg) (*atomic output*) end;
|
wenzelm@25554
|
40 |
|
wenzelm@25554
|
41 |
in
|
wenzelm@25554
|
42 |
|
wenzelm@34102
|
43 |
fun standard_message out_stream ch body =
|
wenzelm@34102
|
44 |
message out_stream ch (Position.properties_of (Position.thread_data ())) body;
|
wenzelm@25554
|
45 |
|
wenzelm@28044
|
46 |
fun init_message out_stream =
|
wenzelm@34214
|
47 |
message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
|
wenzelm@25748
|
48 |
|
wenzelm@25554
|
49 |
end;
|
wenzelm@25554
|
50 |
|
wenzelm@25554
|
51 |
|
wenzelm@25841
|
52 |
(* channels *)
|
wenzelm@25841
|
53 |
|
wenzelm@28188
|
54 |
local
|
wenzelm@28188
|
55 |
|
wenzelm@28188
|
56 |
fun auto_flush stream =
|
wenzelm@28188
|
57 |
let
|
wenzelm@28189
|
58 |
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
|
wenzelm@28188
|
59 |
fun loop () =
|
wenzelm@28188
|
60 |
(OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
|
wenzelm@28188
|
61 |
in loop end;
|
wenzelm@28188
|
62 |
|
wenzelm@28188
|
63 |
in
|
wenzelm@28188
|
64 |
|
wenzelm@28044
|
65 |
fun setup_channels out =
|
wenzelm@28189
|
66 |
let
|
wenzelm@34102
|
67 |
val path = File.platform_path (Path.explode out);
|
wenzelm@34102
|
68 |
val out_stream = TextIO.openOut path; (*fifo blocks until reader is ready*)
|
wenzelm@34102
|
69 |
val _ = OS.FileSys.remove path; (*prevent alien access, indicate writer is ready*)
|
wenzelm@37216
|
70 |
val _ = Simple_Thread.fork false (auto_flush out_stream);
|
wenzelm@37216
|
71 |
val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
|
wenzelm@37216
|
72 |
val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
|
wenzelm@28044
|
73 |
in
|
wenzelm@34102
|
74 |
Output.status_fn := standard_message out_stream "B";
|
wenzelm@34102
|
75 |
Output.writeln_fn := standard_message out_stream "C";
|
wenzelm@37121
|
76 |
Output.tracing_fn := standard_message out_stream "D";
|
wenzelm@37121
|
77 |
Output.warning_fn := standard_message out_stream "E";
|
wenzelm@37121
|
78 |
Output.error_fn := standard_message out_stream "F";
|
wenzelm@37121
|
79 |
Output.debug_fn := standard_message out_stream "G";
|
wenzelm@37121
|
80 |
Output.priority_fn := ! Output.writeln_fn;
|
wenzelm@28498
|
81 |
Output.prompt_fn := ignore;
|
wenzelm@28044
|
82 |
out_stream
|
wenzelm@28044
|
83 |
end;
|
wenzelm@25841
|
84 |
|
wenzelm@28188
|
85 |
end;
|
wenzelm@28188
|
86 |
|
wenzelm@25841
|
87 |
|
wenzelm@25554
|
88 |
(* init *)
|
wenzelm@25554
|
89 |
|
wenzelm@28044
|
90 |
fun init out =
|
wenzelm@34251
|
91 |
(Unsynchronized.change print_mode
|
wenzelm@36950
|
92 |
(fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]);
|
wenzelm@28044
|
93 |
setup_channels out |> init_message;
|
wenzelm@37703
|
94 |
quick_and_dirty := true; (* FIXME !? *)
|
wenzelm@36950
|
95 |
Keyword.report ();
|
wenzelm@31384
|
96 |
Output.status (Markup.markup Markup.ready "");
|
wenzelm@26643
|
97 |
Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
|
wenzelm@25528
|
98 |
|
wenzelm@25528
|
99 |
end;
|