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