(* Title: Pure/Tools/isabelle_process.ML
ID: $Id$
Author: Makarius
Isabelle process wrapper -- interaction via external program.
General format of process output:
(a) unmarked stdout/stderr, no line structure (output should be
processed immediately as it arrives)
(b) echo of my pid on stdout, appears *relatively* early after
startup on a separate line, e.g. "\nPID=4711\n"
(c) properly marked-up messages, e.g. for writeln channel
"\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
where the props consist of name=value lines terminated by "\002,"
each, and the remaining text is any number of lines (output is
supposed to be processed in one piece).
*)
signature ISABELLE_PROCESS =
sig
val test_markupN: string
val test_markup: Markup.T -> output * output
val isabelle_processN: string
val init: unit -> unit
end;
structure IsabelleProcess: ISABELLE_PROCESS =
struct
(* test_markup *)
val test_markupN = "test_markup";
fun test_markup (name, props) =
(enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
enclose "</" ">" name);
val _ = Markup.add_mode test_markupN test_markup;
(* channels *)
val isabelle_processN = "isabelle_process";
local
fun special c = chr 2 ^ c;
val special_sep = special ",";
val special_end = special ".";
fun message_props () =
let
val thread_props = Toplevel.thread_properties ();
val props =
(case AList.lookup (op =) thread_props Markup.idN of
SOME id => [(Markup.idN, id)]
| NONE => Position.properties_of (#1 (Position.of_properties thread_props)));
in implode (map (fn (x, y) => x ^ "=" ^ y ^ special_sep ^ "\n") props) end;
fun output ch markup txt =
Output.writeln_default (special ch ^ message_props () ^ Markup.enclose markup txt ^ special_end);
in
fun setup_channels () =
(Output.writeln_fn := output "A" Markup.writeln;
Output.priority_fn := output "B" Markup.priority;
Output.tracing_fn := output "C" Markup.tracing;
Output.warning_fn := output "D" Markup.warning;
Output.error_fn := output "E" Markup.error;
Output.debug_fn := output "F" Markup.debug);
val _ = Markup.add_mode isabelle_processN (fn (name, _) =>
if name = Markup.promptN then (special "G", special_end ^ "\n")
else ("", ""));
end;
(* init *)
fun init () =
(Output.writeln_default ("\nPID=" ^ string_of_pid (Posix.ProcEnv.getpid ()));
setup_channels ();
change print_mode (update (op =) isabelle_processN);
Isar.secure_main ());
end;