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