src/Pure/Tools/isabelle_process.ML
author wenzelm
Thu Jan 03 17:50:44 2008 +0100 (2008-01-03 ago)
changeset 25810 bac99880fa99
parent 25748 55a458a31e37
child 25820 8228b198c49e
permissions -rw-r--r--
output message properties: id or position;
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@25810
    16
wenzelm@25810
    17
  "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
wenzelm@25810
    18
wenzelm@25810
    19
  where the props consist of name=value lines terminated by "\002,"
wenzelm@25810
    20
  each, and the remaining text is any number of lines (output is
wenzelm@25810
    21
  supposed to be processed in one piece).
wenzelm@25528
    22
*)
wenzelm@25528
    23
wenzelm@25528
    24
signature ISABELLE_PROCESS =
wenzelm@25528
    25
sig
wenzelm@25554
    26
  val test_markupN: string
wenzelm@25554
    27
  val test_markup: Markup.T -> output * output
wenzelm@25748
    28
  val isabelle_processN: string
wenzelm@25528
    29
  val init: unit -> unit
wenzelm@25528
    30
end;
wenzelm@25528
    31
wenzelm@25528
    32
structure IsabelleProcess: ISABELLE_PROCESS =
wenzelm@25528
    33
struct
wenzelm@25528
    34
wenzelm@25748
    35
(* test_markup *)
wenzelm@25554
    36
wenzelm@25554
    37
val test_markupN = "test_markup";
wenzelm@25554
    38
wenzelm@25554
    39
fun test_markup (name, props) =
wenzelm@25554
    40
 (enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
wenzelm@25554
    41
  enclose "</" ">" name);
wenzelm@25554
    42
wenzelm@25554
    43
val _ = Markup.add_mode test_markupN test_markup;
wenzelm@25554
    44
wenzelm@25554
    45
wenzelm@25554
    46
(* channels *)
wenzelm@25554
    47
wenzelm@25748
    48
val isabelle_processN = "isabelle_process";
wenzelm@25748
    49
wenzelm@25554
    50
local
wenzelm@25554
    51
wenzelm@25554
    52
fun special c = chr 2 ^ c;
wenzelm@25810
    53
val special_sep = special ",";
wenzelm@25576
    54
val special_end = special ".";
wenzelm@25554
    55
wenzelm@25810
    56
fun message_props () =
wenzelm@25810
    57
  let
wenzelm@25810
    58
    val thread_props = Toplevel.thread_properties ();
wenzelm@25810
    59
    val props =
wenzelm@25810
    60
      (case AList.lookup (op =) thread_props Markup.idN of
wenzelm@25810
    61
        SOME id => [(Markup.idN, id)]
wenzelm@25810
    62
      | NONE => Position.properties_of (#1 (Position.of_properties thread_props)));
wenzelm@25810
    63
  in implode (map (fn (x, y) => x ^ "=" ^ y ^ special_sep ^ "\n") props) end;
wenzelm@25810
    64
wenzelm@25810
    65
fun output ch markup txt =
wenzelm@25810
    66
  Output.writeln_default (special ch ^ message_props () ^ Markup.enclose markup txt ^ special_end);
wenzelm@25554
    67
wenzelm@25554
    68
in
wenzelm@25554
    69
wenzelm@25554
    70
fun setup_channels () =
wenzelm@25554
    71
 (Output.writeln_fn  := output "A" Markup.writeln;
wenzelm@25554
    72
  Output.priority_fn := output "B" Markup.priority;
wenzelm@25554
    73
  Output.tracing_fn  := output "C" Markup.tracing;
wenzelm@25554
    74
  Output.warning_fn  := output "D" Markup.warning;
wenzelm@25554
    75
  Output.error_fn    := output "E" Markup.error;
wenzelm@25554
    76
  Output.debug_fn    := output "F" Markup.debug);
wenzelm@25554
    77
wenzelm@25748
    78
val _ = Markup.add_mode isabelle_processN (fn (name, _) =>
wenzelm@25748
    79
  if name = Markup.promptN then (special "G", special_end ^ "\n")
wenzelm@25748
    80
  else ("", ""));
wenzelm@25748
    81
wenzelm@25554
    82
end;
wenzelm@25554
    83
wenzelm@25554
    84
wenzelm@25554
    85
(* init *)
wenzelm@25554
    86
wenzelm@25528
    87
fun init () =
wenzelm@25631
    88
 (Output.writeln_default ("\nPID=" ^ string_of_pid (Posix.ProcEnv.getpid ()));
wenzelm@25554
    89
  setup_channels ();
wenzelm@25748
    90
  change print_mode (update (op =) isabelle_processN);
wenzelm@25528
    91
  Isar.secure_main ());
wenzelm@25528
    92
wenzelm@25528
    93
end;
wenzelm@25528
    94