src/Pure/Tools/isabelle_process.ML
author wenzelm
Sat Jan 05 21:37:24 2008 +0100 (2008-01-05 ago)
changeset 25841 af7566faaa0f
parent 25820 8228b198c49e
child 25842 fdabeed7ccd9
permissions -rw-r--r--
added symbol output mode, with XML escapes;
improved message markup: get first position from body text;
added INIT message, with pid and session property;
removed adhoc PID handling;
tuned;
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@25841
    12
  (b) properly marked-up messages, e.g. for writeln channel
wenzelm@25810
    13
wenzelm@25810
    14
  "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
wenzelm@25810
    15
wenzelm@25841
    16
  where the props consist of name=value lines terminated by "\002,\n"
wenzelm@25810
    17
  each, and the remaining text is any number of lines (output is
wenzelm@25810
    18
  supposed to be processed in one piece).
wenzelm@25841
    19
wenzelm@25841
    20
  (c) Special init message holds "pid" and "session" property.
wenzelm@25528
    21
*)
wenzelm@25528
    22
wenzelm@25528
    23
signature ISABELLE_PROCESS =
wenzelm@25528
    24
sig
wenzelm@25554
    25
  val test_markupN: string
wenzelm@25554
    26
  val test_markup: Markup.T -> output * output
wenzelm@25748
    27
  val isabelle_processN: string
wenzelm@25528
    28
  val init: unit -> unit
wenzelm@25528
    29
end;
wenzelm@25528
    30
wenzelm@25528
    31
structure IsabelleProcess: ISABELLE_PROCESS =
wenzelm@25528
    32
struct
wenzelm@25528
    33
wenzelm@25748
    34
(* test_markup *)
wenzelm@25554
    35
wenzelm@25554
    36
val test_markupN = "test_markup";
wenzelm@25554
    37
wenzelm@25554
    38
fun test_markup (name, props) =
wenzelm@25554
    39
 (enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
wenzelm@25554
    40
  enclose "</" ">" name);
wenzelm@25554
    41
wenzelm@25554
    42
val _ = Markup.add_mode test_markupN test_markup;
wenzelm@25554
    43
wenzelm@25554
    44
wenzelm@25841
    45
(* symbol output *)
wenzelm@25554
    46
wenzelm@25748
    47
val isabelle_processN = "isabelle_process";
wenzelm@25748
    48
wenzelm@25554
    49
local
wenzelm@25554
    50
wenzelm@25841
    51
fun output str =
wenzelm@25841
    52
  let
wenzelm@25841
    53
    fun out s = if Symbol.is_raw s then Symbol.decode_raw s else XML.text s;
wenzelm@25841
    54
    val syms = Symbol.explode str;
wenzelm@25841
    55
  in (implode (map out syms), Symbol.length syms) end;
wenzelm@25841
    56
wenzelm@25841
    57
in
wenzelm@25841
    58
wenzelm@25841
    59
val _ = Output.add_mode isabelle_processN output Symbol.encode_raw;
wenzelm@25841
    60
wenzelm@25841
    61
end;
wenzelm@25841
    62
wenzelm@25841
    63
wenzelm@25841
    64
(* message markup *)
wenzelm@25841
    65
wenzelm@25841
    66
val STX = chr 2;
wenzelm@25841
    67
val DEL = chr 127;
wenzelm@25841
    68
wenzelm@25841
    69
fun special ch = STX ^ ch;
wenzelm@25810
    70
val special_sep = special ",";
wenzelm@25576
    71
val special_end = special ".";
wenzelm@25554
    72
wenzelm@25841
    73
local
wenzelm@25810
    74
wenzelm@25841
    75
fun print_props props =
wenzelm@25841
    76
  let
wenzelm@25841
    77
    val clean = translate_string (fn c =>
wenzelm@25841
    78
      if c = STX orelse c = "\n" orelse c = "\r" then DEL else c);
wenzelm@25841
    79
  in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
wenzelm@25841
    80
wenzelm@25841
    81
fun get_pos (elem as XML.Elem (name, atts, ts)) =
wenzelm@25841
    82
      if name = Markup.positionN then SOME (Position.of_properties atts)
wenzelm@25841
    83
      else get_first get_pos ts
wenzelm@25841
    84
  | get_pos _ = NONE;
wenzelm@25554
    85
wenzelm@25554
    86
in
wenzelm@25554
    87
wenzelm@25841
    88
fun message ch markup raw_txt =
wenzelm@25841
    89
  let
wenzelm@25841
    90
    val (txt, pos) =
wenzelm@25841
    91
      (case try XML.tree_of_string (XML.element "message" [] [raw_txt]) of
wenzelm@25841
    92
        NONE => (raw_txt, Position.none)
wenzelm@25841
    93
      | SOME xml => (XML.plain_content xml, the_default Position.none (get_pos xml)))
wenzelm@25841
    94
      |>> translate_string (fn c => if c = STX then DEL else c);
wenzelm@25841
    95
    val props =
wenzelm@25841
    96
      (case Position.properties_of (Position.thread_data ()) of
wenzelm@25841
    97
        [] => Position.properties_of pos
wenzelm@25841
    98
      | props => props);
wenzelm@25841
    99
    val s = special ch ^ print_props props ^ Markup.enclose markup txt ^ special_end;
wenzelm@25841
   100
  in Output.writeln_default s end;
wenzelm@25554
   101
wenzelm@25841
   102
fun init_message () =
wenzelm@25841
   103
  let
wenzelm@25841
   104
    val pid = string_of_pid (Posix.ProcEnv.getpid ());
wenzelm@25841
   105
    val session = List.last (Session.id ()) handle List.Empty => "unknown";
wenzelm@25841
   106
    val welcome = Session.welcome ();
wenzelm@25841
   107
    val s = special "H" ^ print_props [("pid", pid), ("session", session)] ^ welcome ^ special_end;
wenzelm@25841
   108
  in Output.writeln_default s end;
wenzelm@25748
   109
wenzelm@25554
   110
end;
wenzelm@25554
   111
wenzelm@25554
   112
wenzelm@25841
   113
(* channels *)
wenzelm@25841
   114
wenzelm@25841
   115
fun setup_channels () =
wenzelm@25841
   116
 (Output.writeln_fn  := message "A" Markup.writeln;
wenzelm@25841
   117
  Output.priority_fn := message "B" Markup.priority;
wenzelm@25841
   118
  Output.tracing_fn  := message "C" Markup.tracing;
wenzelm@25841
   119
  Output.warning_fn  := message "D" Markup.warning;
wenzelm@25841
   120
  Output.error_fn    := message "E" Markup.error;
wenzelm@25841
   121
  Output.debug_fn    := message "F" Markup.debug);
wenzelm@25841
   122
wenzelm@25841
   123
val _ = Markup.add_mode isabelle_processN (fn (name, props) =>
wenzelm@25841
   124
  if name = Markup.promptN then (special "G", special_end ^ "\n")
wenzelm@25841
   125
  else if name = Markup.positionN then test_markup (name, props)
wenzelm@25841
   126
  else ("", ""));
wenzelm@25841
   127
wenzelm@25841
   128
wenzelm@25554
   129
(* init *)
wenzelm@25554
   130
wenzelm@25528
   131
fun init () =
wenzelm@25841
   132
 (change print_mode (update (op =) isabelle_processN);
wenzelm@25554
   133
  setup_channels ();
wenzelm@25841
   134
  init_message ();
wenzelm@25528
   135
  Isar.secure_main ());
wenzelm@25528
   136
wenzelm@25528
   137
end;
wenzelm@25528
   138