src/Pure/Tools/isabelle_process.ML
author wenzelm
Tue, 08 Apr 2008 11:59:25 +0200
changeset 26574 560d07845442
parent 26550 a8740ad422d2
child 26607 e36d16985402
permissions -rw-r--r--
support "YXML" mode for output transfer notation; 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
25842
fdabeed7ccd9 tuned comments;
wenzelm
parents: 25841
diff changeset
    10
  processed immediately as it arrives);
25631
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
25842
fdabeed7ccd9 tuned comments;
wenzelm
parents: 25841
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
25842
fdabeed7ccd9 tuned comments;
wenzelm
parents: 25841
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
26574
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    25
  val isabelle_processN: string
26208
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
    26
  val full_markupN: string
26574
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    27
  val yxmlN: 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
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    34
(* print modes *)
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    35
25748
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    36
val isabelle_processN = "isabelle_process";
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    37
val full_markupN = "full_markup";
26574
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    38
val yxmlN = "YXML";
25748
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    39
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    40
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    41
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    42
val _ = Markup.add_mode isabelle_processN (fn (name, props) =>
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    43
  if print_mode_active full_markupN orelse name = Markup.positionN
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    44
  then YXML.output_markup (name, props) else ("", ""));
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    45
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    46
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    47
(* message markup *)
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    48
26527
c392354a1b79 Symbol.STX, Symbol.DEL;
wenzelm
parents: 26463
diff changeset
    49
fun special ch = Symbol.STX ^ ch;
25810
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    50
val special_sep = special ",";
25576
ee11881606b7 special_end: replaced Z by dot;
wenzelm
parents: 25565
diff changeset
    51
val special_end = special ".";
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    52
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    53
local
25810
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    54
26574
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    55
fun clean_string bad str =
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    56
  if exists_string (member (op =) bad) str then
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    57
    translate_string (fn c => if member (op =) bad c then Symbol.DEL else c) str
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    58
  else str;
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    59
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    60
fun message_props props =
26574
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    61
  let val clean = clean_string [Symbol.STX, "\n", "\r"]
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    62
  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
    63
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    64
fun message_text ts =
26574
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    65
  let
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    66
    val doc = XML.Elem ("message", [], ts);
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    67
    val msg =
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    68
      if not (print_mode_active full_markupN) then
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    69
        Buffer.content (fold XML.add_content ts Buffer.empty)
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    70
      else if print_mode_active yxmlN then YXML.string_of doc
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    71
      else XML.header ^ XML.string_of doc;
560d07845442 support "YXML" mode for output transfer notation;
wenzelm
parents: 26550
diff changeset
    72
  in clean_string [Symbol.STX] msg end;
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    73
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    74
fun message_pos ts = get_first get_pos ts
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    75
and get_pos (elem as XML.Elem (name, atts, ts)) =
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    76
      if name = Markup.positionN then SOME (Position.of_properties atts)
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    77
      else message_pos ts
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    78
  | get_pos _ = NONE
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    79
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    80
in
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    81
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    82
fun message ch body =
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    83
  let
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    84
    val (txt, pos) =
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    85
      let val ts = YXML.parse_body body
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    86
      in (message_text ts, the_default Position.none (message_pos ts)) end
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    87
      handle Fail msg => ("*** MALFORMED MESSAGE ***\n" ^ msg, Position.none);
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    88
    val props =
26053
f8ee5cbb3068 tuned default position;
wenzelm
parents: 25849
diff changeset
    89
      Position.properties_of (Position.thread_data ())
f8ee5cbb3068 tuned default position;
wenzelm
parents: 25849
diff changeset
    90
      |> Position.default_properties pos;
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    91
  in Output.writeln_default (special ch ^ message_props props ^ txt ^ special_end) end;
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    92
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    93
fun init_message () =
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    94
  let
25849
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
    95
    val pid = ("pid", string_of_pid (Posix.ProcEnv.getpid ()));
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
    96
    val session = ("session", List.last (Session.id ()) handle List.Empty => "unknown");
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    97
    val welcome = Session.welcome ();
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
    98
  in Output.writeln_default (special "H" ^ message_props [pid, session] ^ welcome ^ special_end) end;
25748
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    99
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
   100
end;
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
   101
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
   102
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   103
(* channels *)
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   104
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   105
fun setup_channels () =
25849
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   106
 (Output.writeln_fn  := message "A";
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   107
  Output.priority_fn := message "B";
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   108
  Output.tracing_fn  := message "C";
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   109
  Output.warning_fn  := message "D";
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   110
  Output.error_fn    := message "E";
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   111
  Output.debug_fn    := message "F";
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   112
  Output.prompt_fn   := message "G");
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   113
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   114
26208
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   115
(* token translations *)
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   116
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   117
local
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   118
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   119
fun markup kind x =
26550
a8740ad422d2 removed yxmlN for now;
wenzelm
parents: 26543
diff changeset
   120
  ((YXML.output_markup (kind, []) |-> enclose) (Output.output x), Symbol.length (Symbol.explode x));
26208
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   121
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   122
fun free_or_skolem x =
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   123
  (case try Name.dest_skolem x of
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   124
    NONE => markup Markup.freeN x
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   125
  | SOME x' => markup Markup.skolemN x');
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   126
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   127
fun var_or_skolem s =
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   128
  (case Lexicon.read_variable s of
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   129
    SOME (x, i) =>
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   130
      (case try Name.dest_skolem x of
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   131
        NONE => markup Markup.varN s
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   132
      | SOME x' => markup Markup.skolemN
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   133
          (setmp show_question_marks true Term.string_of_vname (x', i)))
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   134
  | NONE => markup Markup.varN s);
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   135
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   136
val token_trans =
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   137
 Syntax.tokentrans_mode full_markupN
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   138
  [("class", markup Markup.classN),
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   139
   ("tfree", markup Markup.tfreeN),
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   140
   ("tvar", markup Markup.tvarN),
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   141
   ("free", free_or_skolem),
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   142
   ("bound", markup Markup.boundN),
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   143
   ("var", var_or_skolem)];
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   144
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   145
in
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   146
26463
9283b4185fdf Context.>> : operate on Context.generic;
wenzelm
parents: 26435
diff changeset
   147
val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans));
26208
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   148
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   149
end;
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   150
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   151
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
   152
(* init *)
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
   153
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
   154
fun init () =
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   155
 (change print_mode (update (op =) isabelle_processN);
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
   156
  setup_channels ();
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   157
  init_message ();
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
   158
  Isar.secure_main ());
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
   159
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
   160
end;
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
   161