src/Pure/Tools/isabelle_process.ML
author wenzelm
Sun Dec 30 23:07:27 2007 +0100 (2007-12-30 ago)
changeset 25748 55a458a31e37
parent 25631 9036ccd685b4
child 25810 bac99880fa99
permissions -rw-r--r--
added PROMPT message;
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