author | wenzelm |
Fri, 14 Dec 2007 21:15:37 +0100 | |
changeset 25631 | 9036ccd685b4 |
parent 25576 | ee11881606b7 |
child 25748 | 55a458a31e37 |
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 |
|
16 |
"\002A" ^ text ^ "\002.\n" where the body text may consist of several |
|
17 |
lines (output should be processed in one piece). |
|
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
18 |
*) |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
19 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
20 |
signature ISABELLE_PROCESS = |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
21 |
sig |
25554 | 22 |
val test_markupN: string |
23 |
val test_markup: Markup.T -> output * output |
|
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
24 |
val init: unit -> unit |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
25 |
end; |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
26 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
27 |
structure IsabelleProcess: ISABELLE_PROCESS = |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
28 |
struct |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
29 |
|
25554 | 30 |
(* test markup *) |
31 |
||
32 |
val test_markupN = "test_markup"; |
|
33 |
||
34 |
fun test_markup (name, props) = |
|
35 |
(enclose "<" ">" (space_implode " " (name :: map XML.attribute props)), |
|
36 |
enclose "</" ">" name); |
|
37 |
||
38 |
val _ = Markup.add_mode test_markupN test_markup; |
|
39 |
||
40 |
||
41 |
(* channels *) |
|
42 |
||
43 |
local |
|
44 |
||
45 |
fun special c = chr 2 ^ c; |
|
25576 | 46 |
val special_end = special "."; |
25554 | 47 |
|
48 |
fun output c m s = |
|
49 |
Output.writeln_default (special c ^ Markup.enclose m s ^ special_end); |
|
50 |
||
51 |
in |
|
52 |
||
53 |
fun setup_channels () = |
|
54 |
(Output.writeln_fn := output "A" Markup.writeln; |
|
55 |
Output.priority_fn := output "B" Markup.priority; |
|
56 |
Output.tracing_fn := output "C" Markup.tracing; |
|
57 |
Output.warning_fn := output "D" Markup.warning; |
|
58 |
Output.error_fn := output "E" Markup.error; |
|
59 |
Output.debug_fn := output "F" Markup.debug); |
|
60 |
||
61 |
end; |
|
62 |
||
63 |
||
64 |
(* init *) |
|
65 |
||
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
66 |
fun init () = |
25631 | 67 |
(Output.writeln_default ("\nPID=" ^ string_of_pid (Posix.ProcEnv.getpid ())); |
25554 | 68 |
setup_channels (); |
25528
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
69 |
Isar.secure_main ()); |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
70 |
|
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
71 |
end; |
e67230c2b952
Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff
changeset
|
72 |