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