wenzelm@30174
|
1 |
(* Title: Pure/System/isabelle_process.ML
|
wenzelm@25528
|
2 |
Author: Makarius
|
wenzelm@25528
|
3 |
|
wenzelm@25528
|
4 |
Isabelle process wrapper -- interaction via external program.
|
wenzelm@25631
|
5 |
|
wenzelm@25631
|
6 |
General format of process output:
|
wenzelm@25631
|
7 |
|
wenzelm@29328
|
8 |
(1) unmarked stdout/stderr, no line structure (output should be
|
wenzelm@25842
|
9 |
processed immediately as it arrives);
|
wenzelm@25631
|
10 |
|
wenzelm@29328
|
11 |
(2) properly marked-up messages, e.g. for writeln channel
|
wenzelm@25810
|
12 |
|
wenzelm@25810
|
13 |
"\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
|
wenzelm@25810
|
14 |
|
wenzelm@25841
|
15 |
where the props consist of name=value lines terminated by "\002,\n"
|
wenzelm@25810
|
16 |
each, and the remaining text is any number of lines (output is
|
wenzelm@25842
|
17 |
supposed to be processed in one piece);
|
wenzelm@25841
|
18 |
|
wenzelm@29328
|
19 |
(3) special init message holds "pid" and "session" property;
|
wenzelm@29328
|
20 |
|
wenzelm@29328
|
21 |
(4) message content is encoded in YXML format.
|
wenzelm@25528
|
22 |
*)
|
wenzelm@25528
|
23 |
|
wenzelm@25528
|
24 |
signature ISABELLE_PROCESS =
|
wenzelm@25528
|
25 |
sig
|
wenzelm@26574
|
26 |
val isabelle_processN: string
|
wenzelm@28044
|
27 |
val init: string -> unit
|
wenzelm@25528
|
28 |
end;
|
wenzelm@25528
|
29 |
|
wenzelm@25528
|
30 |
structure IsabelleProcess: ISABELLE_PROCESS =
|
wenzelm@25528
|
31 |
struct
|
wenzelm@25528
|
32 |
|
wenzelm@26550
|
33 |
(* print modes *)
|
wenzelm@25554
|
34 |
|
wenzelm@25748
|
35 |
val isabelle_processN = "isabelle_process";
|
wenzelm@25748
|
36 |
|
wenzelm@26550
|
37 |
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
|
wenzelm@28036
|
38 |
val _ = Markup.add_mode isabelle_processN YXML.output_markup;
|
wenzelm@25841
|
39 |
|
wenzelm@25841
|
40 |
|
wenzelm@25841
|
41 |
(* message markup *)
|
wenzelm@25841
|
42 |
|
wenzelm@26527
|
43 |
fun special ch = Symbol.STX ^ ch;
|
wenzelm@25810
|
44 |
val special_sep = special ",";
|
wenzelm@25576
|
45 |
val special_end = special ".";
|
wenzelm@25554
|
46 |
|
wenzelm@25841
|
47 |
local
|
wenzelm@25810
|
48 |
|
wenzelm@26574
|
49 |
fun clean_string bad str =
|
wenzelm@26574
|
50 |
if exists_string (member (op =) bad) str then
|
wenzelm@26574
|
51 |
translate_string (fn c => if member (op =) bad c then Symbol.DEL else c) str
|
wenzelm@26574
|
52 |
else str;
|
wenzelm@26574
|
53 |
|
wenzelm@26550
|
54 |
fun message_props props =
|
wenzelm@26574
|
55 |
let val clean = clean_string [Symbol.STX, "\n", "\r"]
|
wenzelm@25841
|
56 |
in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
|
wenzelm@25841
|
57 |
|
wenzelm@29328
|
58 |
fun message_pos trees = trees |> get_first
|
wenzelm@29328
|
59 |
(fn XML.Elem (name, atts, ts) =>
|
wenzelm@29328
|
60 |
if name = Markup.positionN then SOME (Position.of_properties atts)
|
wenzelm@29328
|
61 |
else message_pos ts
|
wenzelm@29328
|
62 |
| _ => NONE);
|
wenzelm@25554
|
63 |
|
wenzelm@28044
|
64 |
fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
|
wenzelm@28182
|
65 |
(TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
|
wenzelm@28044
|
66 |
|
wenzelm@25554
|
67 |
in
|
wenzelm@25554
|
68 |
|
wenzelm@29522
|
69 |
fun message _ _ "" = ()
|
wenzelm@29522
|
70 |
| message out_stream ch body =
|
wenzelm@27844
|
71 |
let
|
wenzelm@29329
|
72 |
val pos = the_default Position.none (message_pos (YXML.parse_body body));
|
wenzelm@27844
|
73 |
val props =
|
wenzelm@27844
|
74 |
Position.properties_of (Position.thread_data ())
|
wenzelm@27844
|
75 |
|> Position.default_properties pos;
|
wenzelm@29522
|
76 |
val txt = clean_string [Symbol.STX] body;
|
wenzelm@28044
|
77 |
in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
|
wenzelm@25554
|
78 |
|
wenzelm@28044
|
79 |
fun init_message out_stream =
|
wenzelm@25841
|
80 |
let
|
wenzelm@28491
|
81 |
val pid = (Markup.pidN, process_id ());
|
wenzelm@27972
|
82 |
val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
|
wenzelm@29522
|
83 |
val text = Session.welcome ();
|
wenzelm@28343
|
84 |
in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
|
wenzelm@25748
|
85 |
|
wenzelm@25554
|
86 |
end;
|
wenzelm@25554
|
87 |
|
wenzelm@25554
|
88 |
|
wenzelm@25841
|
89 |
(* channels *)
|
wenzelm@25841
|
90 |
|
wenzelm@28188
|
91 |
local
|
wenzelm@28188
|
92 |
|
wenzelm@28188
|
93 |
fun auto_flush stream =
|
wenzelm@28188
|
94 |
let
|
wenzelm@28189
|
95 |
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
|
wenzelm@28188
|
96 |
fun loop () =
|
wenzelm@28188
|
97 |
(OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
|
wenzelm@28188
|
98 |
in loop end;
|
wenzelm@28188
|
99 |
|
wenzelm@28188
|
100 |
in
|
wenzelm@28188
|
101 |
|
wenzelm@28044
|
102 |
fun setup_channels out =
|
wenzelm@28189
|
103 |
let
|
wenzelm@28189
|
104 |
val out_stream =
|
wenzelm@28189
|
105 |
if out = "-" then TextIO.stdOut
|
wenzelm@28189
|
106 |
else
|
wenzelm@28189
|
107 |
let
|
wenzelm@28189
|
108 |
val path = File.platform_path (Path.explode out);
|
wenzelm@28189
|
109 |
val out_stream = TextIO.openOut path; (*fifo blocks until reader is ready*)
|
wenzelm@28189
|
110 |
val _ = OS.FileSys.remove path; (*prevent alien access, indicate writer is ready*)
|
wenzelm@28242
|
111 |
val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
|
wenzelm@28189
|
112 |
in out_stream end;
|
wenzelm@28242
|
113 |
val _ = SimpleThread.fork false (auto_flush out_stream);
|
wenzelm@28242
|
114 |
val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
|
wenzelm@28044
|
115 |
in
|
wenzelm@29522
|
116 |
Output.status_fn := message out_stream "B";
|
wenzelm@29522
|
117 |
Output.writeln_fn := message out_stream "C";
|
wenzelm@29522
|
118 |
Output.priority_fn := message out_stream "D";
|
wenzelm@29522
|
119 |
Output.tracing_fn := message out_stream "E";
|
wenzelm@29522
|
120 |
Output.warning_fn := message out_stream "F";
|
wenzelm@29522
|
121 |
Output.error_fn := message out_stream "G";
|
wenzelm@29522
|
122 |
Output.debug_fn := message out_stream "H";
|
wenzelm@28498
|
123 |
Output.prompt_fn := ignore;
|
wenzelm@28044
|
124 |
out_stream
|
wenzelm@28044
|
125 |
end;
|
wenzelm@25841
|
126 |
|
wenzelm@28188
|
127 |
end;
|
wenzelm@28188
|
128 |
|
wenzelm@25841
|
129 |
|
wenzelm@25554
|
130 |
(* init *)
|
wenzelm@25554
|
131 |
|
wenzelm@28044
|
132 |
fun init out =
|
wenzelm@25841
|
133 |
(change print_mode (update (op =) isabelle_processN);
|
wenzelm@28044
|
134 |
setup_channels out |> init_message;
|
wenzelm@28342
|
135 |
OuterKeyword.report ();
|
wenzelm@31384
|
136 |
Output.status (Markup.markup Markup.ready "");
|
wenzelm@26643
|
137 |
Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
|
wenzelm@25528
|
138 |
|
wenzelm@25528
|
139 |
end;
|