author | wenzelm |
Thu, 03 Jan 2008 17:50:44 +0100 | |
changeset 25810 | bac99880fa99 |
parent 25748 | 55a458a31e37 |
child 25820 | 8228b198c49e |
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 |
|
10 |
processed immediately as it arrives) |
|
11 |
||
12 |
(b) echo of my pid on stdout, appears *relatively* early after |
|
13 |
startup on a separate line, e.g. "\nPID=4711\n" |
|
14 |
||
15 |
(c) properly marked-up messages, e.g. for writeln channel |
|
25810 | 16 |
|
17 |
"\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n" |
|
18 |
||
19 |
where the props consist of name=value lines terminated by "\002," |
|
20 |
each, and the remaining text is any number of lines (output is |
|
21 |
supposed to be processed in one piece). |
|
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 |
25554 | 26 |
val test_markupN: string |
27 |
val test_markup: Markup.T -> output * output |
|
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 |
|
25748 | 35 |
(* test_markup *) |
25554 | 36 |
|
37 |
val test_markupN = "test_markup"; |
|
38 |
||
39 |
fun test_markup (name, props) = |
|
40 |
(enclose "<" ">" (space_implode " " (name :: map XML.attribute props)), |
|
41 |
enclose "</" ">" name); |
|
42 |
||
43 |
val _ = Markup.add_mode test_markupN test_markup; |
|
44 |
||
45 |
||
46 |
(* channels *) |
|
47 |
||
25748 | 48 |
val isabelle_processN = "isabelle_process"; |
49 |
||
25554 | 50 |
local |
51 |
||
52 |
fun special c = chr 2 ^ c; |
|
25810 | 53 |
val special_sep = special ","; |
25576 | 54 |
val special_end = special "."; |
25554 | 55 |
|
25810 | 56 |
fun message_props () = |
57 |
let |
|
58 |
val thread_props = Toplevel.thread_properties (); |
|
59 |
val props = |
|
60 |
(case AList.lookup (op =) thread_props Markup.idN of |
|
61 |
SOME id => [(Markup.idN, id)] |
|
62 |
| NONE => Position.properties_of (#1 (Position.of_properties thread_props))); |
|
63 |
in implode (map (fn (x, y) => x ^ "=" ^ y ^ special_sep ^ "\n") props) end; |
|
64 |
||
65 |
fun output ch markup txt = |
|
66 |
Output.writeln_default (special ch ^ message_props () ^ Markup.enclose markup txt ^ special_end); |
|
25554 | 67 |
|
68 |
in |
|
69 |
||
70 |
fun setup_channels () = |
|
71 |
(Output.writeln_fn := output "A" Markup.writeln; |
|
72 |
Output.priority_fn := output "B" Markup.priority; |
|
73 |
Output.tracing_fn := output "C" Markup.tracing; |
|
74 |
Output.warning_fn := output "D" Markup.warning; |
|
75 |
Output.error_fn := output "E" Markup.error; |
|
76 |
Output.debug_fn := output "F" Markup.debug); |
|
77 |
||
25748 | 78 |
val _ = Markup.add_mode isabelle_processN (fn (name, _) => |
79 |
if name = Markup.promptN then (special "G", special_end ^ "\n") |
|
80 |
else ("", "")); |
|
81 |
||
25554 | 82 |
end; |
83 |
||
84 |
||
85 |
(* init *) |
|
86 |
||
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
87 |
fun init () = |
25631 | 88 |
(Output.writeln_default ("\nPID=" ^ string_of_pid (Posix.ProcEnv.getpid ())); |
25554 | 89 |
setup_channels (); |
25748 | 90 |
change print_mode (update (op =) isabelle_processN); |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
91 |
Isar.secure_main ()); |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
92 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
93 |
end; |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
94 |