author | wenzelm |
Wed, 05 Mar 2008 22:58:13 +0100 | |
changeset 26208 | 278f47ae70d1 |
parent 26053 | f8ee5cbb3068 |
child 26253 | 0506197d285f |
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 |
26208 | 25 |
val output_markup: Markup.T -> output * output |
26 |
val full_markupN: string |
|
25554 | 27 |
val test_markupN: string |
25748 | 28 |
val isabelle_processN: string |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
29 |
val init: unit -> unit |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
30 |
end; |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
31 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
32 |
structure IsabelleProcess: ISABELLE_PROCESS = |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
33 |
struct |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
34 |
|
26208 | 35 |
(* explicit markup *) |
25554 | 36 |
|
26208 | 37 |
fun output_markup (name, props) = |
25554 | 38 |
(enclose "<" ">" (space_implode " " (name :: map XML.attribute props)), |
39 |
enclose "</" ">" name); |
|
40 |
||
26208 | 41 |
val full_markupN = "full_markup"; |
42 |
val test_markupN = "test_markup"; |
|
43 |
||
44 |
val _ = Markup.add_mode test_markupN output_markup; |
|
25554 | 45 |
|
46 |
||
25841 | 47 |
(* symbol output *) |
25554 | 48 |
|
25748 | 49 |
val isabelle_processN = "isabelle_process"; |
50 |
||
25554 | 51 |
local |
52 |
||
25841 | 53 |
fun output str = |
54 |
let |
|
55 |
fun out s = if Symbol.is_raw s then Symbol.decode_raw s else XML.text s; |
|
56 |
val syms = Symbol.explode str; |
|
57 |
in (implode (map out syms), Symbol.length syms) end; |
|
58 |
||
59 |
in |
|
60 |
||
61 |
val _ = Output.add_mode isabelle_processN output Symbol.encode_raw; |
|
62 |
||
63 |
end; |
|
64 |
||
65 |
||
66 |
(* message markup *) |
|
67 |
||
68 |
val STX = chr 2; |
|
69 |
val DEL = chr 127; |
|
70 |
||
71 |
fun special ch = STX ^ ch; |
|
25810 | 72 |
val special_sep = special ","; |
25576 | 73 |
val special_end = special "."; |
25554 | 74 |
|
25841 | 75 |
local |
25810 | 76 |
|
25841 | 77 |
fun print_props props = |
78 |
let |
|
79 |
val clean = translate_string (fn c => |
|
80 |
if c = STX orelse c = "\n" orelse c = "\r" then DEL else c); |
|
81 |
in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end; |
|
82 |
||
83 |
fun get_pos (elem as XML.Elem (name, atts, ts)) = |
|
84 |
if name = Markup.positionN then SOME (Position.of_properties atts) |
|
85 |
else get_first get_pos ts |
|
86 |
| get_pos _ = NONE; |
|
25554 | 87 |
|
88 |
in |
|
89 |
||
25849 | 90 |
val _ = Markup.add_mode isabelle_processN (fn (name, props) => |
26208 | 91 |
if print_mode_active full_markupN orelse name = Markup.positionN |
92 |
then output_markup (name, props) else ("", "")); |
|
25849 | 93 |
|
94 |
fun message ch raw_txt = |
|
25841 | 95 |
let |
96 |
val (txt, pos) = |
|
97 |
(case try XML.tree_of_string (XML.element "message" [] [raw_txt]) of |
|
98 |
NONE => (raw_txt, Position.none) |
|
26208 | 99 |
| SOME xml => |
100 |
(if print_mode_active full_markupN then XML.header ^ raw_txt else XML.plain_content xml, |
|
101 |
the_default Position.none (get_pos xml))) |
|
25841 | 102 |
|>> translate_string (fn c => if c = STX then DEL else c); |
103 |
val props = |
|
26053 | 104 |
Position.properties_of (Position.thread_data ()) |
105 |
|> Position.default_properties pos; |
|
25849 | 106 |
in Output.writeln_default (special ch ^ print_props props ^ txt ^ special_end) end; |
25554 | 107 |
|
25841 | 108 |
fun init_message () = |
109 |
let |
|
25849 | 110 |
val pid = ("pid", string_of_pid (Posix.ProcEnv.getpid ())); |
111 |
val session = ("session", List.last (Session.id ()) handle List.Empty => "unknown"); |
|
25841 | 112 |
val welcome = Session.welcome (); |
25849 | 113 |
in Output.writeln_default (special "H" ^ print_props [pid, session] ^ welcome ^ special_end) end; |
25748 | 114 |
|
25554 | 115 |
end; |
116 |
||
117 |
||
25841 | 118 |
(* channels *) |
119 |
||
120 |
fun setup_channels () = |
|
25849 | 121 |
(Output.writeln_fn := message "A"; |
122 |
Output.priority_fn := message "B"; |
|
123 |
Output.tracing_fn := message "C"; |
|
124 |
Output.warning_fn := message "D"; |
|
125 |
Output.error_fn := message "E"; |
|
126 |
Output.debug_fn := message "F"; |
|
127 |
Output.prompt_fn := message "G"); |
|
25841 | 128 |
|
129 |
||
26208 | 130 |
(* token translations *) |
131 |
||
132 |
local |
|
133 |
||
134 |
fun markup kind x = |
|
135 |
((output_markup (kind, []) |-> enclose) x, Symbol.length (Symbol.explode x)); |
|
136 |
||
137 |
fun free_or_skolem x = |
|
138 |
(case try Name.dest_skolem x of |
|
139 |
NONE => markup Markup.freeN x |
|
140 |
| SOME x' => markup Markup.skolemN x'); |
|
141 |
||
142 |
fun var_or_skolem s = |
|
143 |
(case Lexicon.read_variable s of |
|
144 |
SOME (x, i) => |
|
145 |
(case try Name.dest_skolem x of |
|
146 |
NONE => markup Markup.varN s |
|
147 |
| SOME x' => markup Markup.skolemN |
|
148 |
(setmp show_question_marks true Term.string_of_vname (x', i))) |
|
149 |
| NONE => markup Markup.varN s); |
|
150 |
||
151 |
val token_trans = |
|
152 |
Syntax.tokentrans_mode full_markupN |
|
153 |
[("class", markup Markup.classN), |
|
154 |
("tfree", markup Markup.tfreeN), |
|
155 |
("tvar", markup Markup.tvarN), |
|
156 |
("free", free_or_skolem), |
|
157 |
("bound", markup Markup.boundN), |
|
158 |
("var", var_or_skolem)]; |
|
159 |
||
160 |
in |
|
161 |
||
162 |
val _ = Context.add_setup (Sign.add_tokentrfuns token_trans); |
|
163 |
||
164 |
end; |
|
165 |
||
25841 | 166 |
|
25554 | 167 |
(* init *) |
168 |
||
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
169 |
fun init () = |
25841 | 170 |
(change print_mode (update (op =) isabelle_processN); |
25554 | 171 |
setup_channels (); |
25841 | 172 |
init_message (); |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
173 |
Isar.secure_main ()); |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
174 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
175 |
end; |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
176 |