author | wenzelm |
Sun, 24 Aug 2008 18:57:43 +0200 | |
changeset 27986 | 26e1a7a6695d |
parent 27972 | a87be8fcb25c |
child 28036 | a58e4da3d184 |
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 |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
27 |
val init: unit -> unit |
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; |
27961 | 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 |
|
73 |
in |
|
74 |
||
27961 | 75 |
fun message _ _ "" = () |
76 |
| message ch class body = |
|
27844 | 77 |
let |
78 |
val (txt, pos) = |
|
79 |
let val ts = YXML.parse_body body |
|
27961 | 80 |
in (message_text class ts, the_default Position.none (message_pos ts)) end; |
27844 | 81 |
val props = |
82 |
Position.properties_of (Position.thread_data ()) |
|
83 |
|> Position.default_properties pos; |
|
84 |
in Output.writeln_default (special ch ^ message_props props ^ txt ^ special_end) end; |
|
25554 | 85 |
|
25841 | 86 |
fun init_message () = |
87 |
let |
|
27972 | 88 |
val pid = (Markup.pidN, string_of_pid (Posix.ProcEnv.getpid ())); |
89 |
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
|
90 |
val text = message_text Markup.initN [XML.Text (Session.welcome ())]; |
26e1a7a6695d
init_message: class markup in message body, not header;
wenzelm
parents:
27972
diff
changeset
|
91 |
in Output.writeln_default (special "H" ^ message_props [pid, session] ^ text ^ special_end) end; |
25748 | 92 |
|
25554 | 93 |
end; |
94 |
||
95 |
||
25841 | 96 |
(* channels *) |
97 |
||
98 |
fun setup_channels () = |
|
27972 | 99 |
(Output.writeln_fn := message "A" Markup.writelnN; |
100 |
Output.priority_fn := message "B" Markup.priorityN; |
|
101 |
Output.tracing_fn := message "C" Markup.tracingN; |
|
102 |
Output.warning_fn := message "D" Markup.warningN; |
|
103 |
Output.error_fn := message "E" Markup.errorN; |
|
104 |
Output.debug_fn := message "F" Markup.debugN; |
|
105 |
Output.prompt_fn := message "G" Markup.promptN; |
|
106 |
Output.status_fn := message "I" Markup.statusN); |
|
25841 | 107 |
|
108 |
||
25554 | 109 |
(* init *) |
110 |
||
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
111 |
fun init () = |
25841 | 112 |
(change print_mode (update (op =) isabelle_processN); |
25554 | 113 |
setup_channels (); |
25841 | 114 |
init_message (); |
26643 | 115 |
Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true}); |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
116 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
117 |
end; |