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