author | wenzelm |
Sun, 30 Dec 2007 23:07:27 +0100 | |
changeset 25748 | 55a458a31e37 |
parent 25631 | 9036ccd685b4 |
child 25810 | bac99880fa99 |
permissions | -rw-r--r-- |
wenzelm@25528 | 1 |
(* Title: Pure/Tools/isabelle_process.ML |
wenzelm@25528 | 2 |
ID: $Id$ |
wenzelm@25528 | 3 |
Author: Makarius |
wenzelm@25528 | 4 |
|
wenzelm@25528 | 5 |
Isabelle process wrapper -- interaction via external program. |
wenzelm@25631 | 6 |
|
wenzelm@25631 | 7 |
General format of process output: |
wenzelm@25631 | 8 |
|
wenzelm@25631 | 9 |
(a) unmarked stdout/stderr, no line structure (output should be |
wenzelm@25631 | 10 |
processed immediately as it arrives) |
wenzelm@25631 | 11 |
|
wenzelm@25631 | 12 |
(b) echo of my pid on stdout, appears *relatively* early after |
wenzelm@25631 | 13 |
startup on a separate line, e.g. "\nPID=4711\n" |
wenzelm@25631 | 14 |
|
wenzelm@25631 | 15 |
(c) properly marked-up messages, e.g. for writeln channel |
wenzelm@25631 | 16 |
"\002A" ^ text ^ "\002.\n" where the body text may consist of several |
wenzelm@25631 | 17 |
lines (output should be processed in one piece). |
wenzelm@25528 | 18 |
*) |
wenzelm@25528 | 19 |
|
wenzelm@25528 | 20 |
signature ISABELLE_PROCESS = |
wenzelm@25528 | 21 |
sig |
wenzelm@25554 | 22 |
val test_markupN: string |
wenzelm@25554 | 23 |
val test_markup: Markup.T -> output * output |
wenzelm@25748 | 24 |
val isabelle_processN: string |
wenzelm@25528 | 25 |
val init: unit -> unit |
wenzelm@25528 | 26 |
end; |
wenzelm@25528 | 27 |
|
wenzelm@25528 | 28 |
structure IsabelleProcess: ISABELLE_PROCESS = |
wenzelm@25528 | 29 |
struct |
wenzelm@25528 | 30 |
|
wenzelm@25748 | 31 |
(* test_markup *) |
wenzelm@25554 | 32 |
|
wenzelm@25554 | 33 |
val test_markupN = "test_markup"; |
wenzelm@25554 | 34 |
|
wenzelm@25554 | 35 |
fun test_markup (name, props) = |
wenzelm@25554 | 36 |
(enclose "<" ">" (space_implode " " (name :: map XML.attribute props)), |
wenzelm@25554 | 37 |
enclose "</" ">" name); |
wenzelm@25554 | 38 |
|
wenzelm@25554 | 39 |
val _ = Markup.add_mode test_markupN test_markup; |
wenzelm@25554 | 40 |
|
wenzelm@25554 | 41 |
|
wenzelm@25554 | 42 |
(* channels *) |
wenzelm@25554 | 43 |
|
wenzelm@25748 | 44 |
val isabelle_processN = "isabelle_process"; |
wenzelm@25748 | 45 |
|
wenzelm@25554 | 46 |
local |
wenzelm@25554 | 47 |
|
wenzelm@25554 | 48 |
fun special c = chr 2 ^ c; |
wenzelm@25576 | 49 |
val special_end = special "."; |
wenzelm@25554 | 50 |
|
wenzelm@25554 | 51 |
fun output c m s = |
wenzelm@25554 | 52 |
Output.writeln_default (special c ^ Markup.enclose m s ^ special_end); |
wenzelm@25554 | 53 |
|
wenzelm@25554 | 54 |
in |
wenzelm@25554 | 55 |
|
wenzelm@25554 | 56 |
fun setup_channels () = |
wenzelm@25554 | 57 |
(Output.writeln_fn := output "A" Markup.writeln; |
wenzelm@25554 | 58 |
Output.priority_fn := output "B" Markup.priority; |
wenzelm@25554 | 59 |
Output.tracing_fn := output "C" Markup.tracing; |
wenzelm@25554 | 60 |
Output.warning_fn := output "D" Markup.warning; |
wenzelm@25554 | 61 |
Output.error_fn := output "E" Markup.error; |
wenzelm@25554 | 62 |
Output.debug_fn := output "F" Markup.debug); |
wenzelm@25554 | 63 |
|
wenzelm@25748 | 64 |
val _ = Markup.add_mode isabelle_processN (fn (name, _) => |
wenzelm@25748 | 65 |
if name = Markup.promptN then (special "G", special_end ^ "\n") |
wenzelm@25748 | 66 |
else ("", "")); |
wenzelm@25748 | 67 |
|
wenzelm@25554 | 68 |
end; |
wenzelm@25554 | 69 |
|
wenzelm@25554 | 70 |
|
wenzelm@25554 | 71 |
(* init *) |
wenzelm@25554 | 72 |
|
wenzelm@25528 | 73 |
fun init () = |
wenzelm@25631 | 74 |
(Output.writeln_default ("\nPID=" ^ string_of_pid (Posix.ProcEnv.getpid ())); |
wenzelm@25554 | 75 |
setup_channels (); |
wenzelm@25748 | 76 |
change print_mode (update (op =) isabelle_processN); |
wenzelm@25528 | 77 |
Isar.secure_main ()); |
wenzelm@25528 | 78 |
|
wenzelm@25528 | 79 |
end; |
wenzelm@25528 | 80 |