author | wenzelm |
Thu, 28 Aug 2008 19:34:51 +0200 | |
changeset 28049 | 6b243f66f688 |
parent 28044 | e4b569b53e10 |
child 28062 | f454a20c1ab1 |
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 () => |
74 |
(TextIO.output (out_stream, s); TextIO.output (out_stream, "\n"); TextIO.flushOut out_stream)); |
|
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 |
||
28044 | 101 |
fun setup_channels out = |
102 |
let val out_stream = |
|
103 |
if out = "" orelse out = "-" then TextIO.stdOut |
|
104 |
else |
|
105 |
let val path = File.platform_path (Path.explode out) |
|
28049 | 106 |
in TextIO.openOut path before OS.FileSys.remove path end; |
28044 | 107 |
in |
108 |
Output.writeln_fn := message out_stream "A" Markup.writelnN; |
|
109 |
Output.priority_fn := message out_stream "B" Markup.priorityN; |
|
110 |
Output.tracing_fn := message out_stream "C" Markup.tracingN; |
|
111 |
Output.warning_fn := message out_stream "D" Markup.warningN; |
|
112 |
Output.error_fn := message out_stream "E" Markup.errorN; |
|
113 |
Output.debug_fn := message out_stream "F" Markup.debugN; |
|
114 |
Output.prompt_fn := message out_stream "G" Markup.promptN; |
|
115 |
Output.status_fn := message out_stream "I" Markup.statusN; |
|
116 |
out_stream |
|
117 |
end; |
|
25841 | 118 |
|
119 |
||
25554 | 120 |
(* init *) |
121 |
||
28044 | 122 |
fun init out = |
25841 | 123 |
(change print_mode (update (op =) isabelle_processN); |
28044 | 124 |
setup_channels out |> init_message; |
26643 | 125 |
Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true}); |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
126 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
127 |
end; |