src/Pure/Tools/isabelle_process.ML
author wenzelm
Thu, 03 Apr 2008 18:42:41 +0200
changeset 26543 cd01c8eb314a
parent 26527 c392354a1b79
child 26550 a8740ad422d2
permissions -rw-r--r--
moved output_markup to xml.ML; added yxmlN mode name;
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
26543
cd01c8eb314a moved output_markup to xml.ML;
wenzelm
parents: 26527
diff changeset
    25
  val yxmlN: string
26208
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
    26
  val full_markupN: string
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    27
  val test_markupN: string
25748
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    28
  val isabelle_processN: string
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    29
  val init: unit -> unit
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    30
end;
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    31
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    32
structure IsabelleProcess: ISABELLE_PROCESS =
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    33
struct
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    34
26208
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
    35
(* explicit markup *)
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    36
26543
cd01c8eb314a moved output_markup to xml.ML;
wenzelm
parents: 26527
diff changeset
    37
val yxmlN = "YXML";
26208
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
    38
val full_markupN = "full_markup";
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
    39
val test_markupN = "test_markup";
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
    40
26543
cd01c8eb314a moved output_markup to xml.ML;
wenzelm
parents: 26527
diff changeset
    41
val _ = Markup.add_mode test_markupN XML.output_markup;
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    42
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    43
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    44
(* symbol output *)
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    45
25748
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    46
val isabelle_processN = "isabelle_process";
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    47
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    48
local
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    49
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    50
fun output str =
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    51
  let
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    52
    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
    53
    val syms = Symbol.explode str;
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    54
  in (implode (map out syms), Symbol.length syms) end;
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    55
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    56
in
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    57
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    58
val _ = Output.add_mode isabelle_processN output Symbol.encode_raw;
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    59
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    60
end;
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    61
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
(* message markup *)
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    64
26527
c392354a1b79 Symbol.STX, Symbol.DEL;
wenzelm
parents: 26463
diff changeset
    65
fun special ch = Symbol.STX ^ ch;
25810
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    66
val special_sep = special ",";
25576
ee11881606b7 special_end: replaced Z by dot;
wenzelm
parents: 25565
diff changeset
    67
val special_end = special ".";
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    68
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    69
local
25810
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    70
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    71
fun print_props props =
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    72
  let
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    73
    val clean = translate_string (fn c =>
26527
c392354a1b79 Symbol.STX, Symbol.DEL;
wenzelm
parents: 26463
diff changeset
    74
      if c = Symbol.STX orelse c = "\n" orelse c = "\r" then Symbol.DEL else c);
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    75
  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
    76
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    77
fun get_pos (elem as XML.Elem (name, atts, ts)) =
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    78
      if name = Markup.positionN then SOME (Position.of_properties atts)
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    79
      else get_first get_pos ts
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    80
  | get_pos _ = NONE;
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    81
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    82
in
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    83
25849
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
    84
val _ = Markup.add_mode isabelle_processN (fn (name, props) =>
26208
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
    85
  if print_mode_active full_markupN orelse name = Markup.positionN
26543
cd01c8eb314a moved output_markup to xml.ML;
wenzelm
parents: 26527
diff changeset
    86
  then XML.output_markup (name, props) else ("", ""));
25849
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
    87
26253
0506197d285f message: proper root element for XML output;
wenzelm
parents: 26208
diff changeset
    88
fun message ch txt0 =
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    89
  let
26253
0506197d285f message: proper root element for XML output;
wenzelm
parents: 26208
diff changeset
    90
    val txt1 = XML.element "message" [] [txt0];
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    91
    val (txt, pos) =
26543
cd01c8eb314a moved output_markup to xml.ML;
wenzelm
parents: 26527
diff changeset
    92
      (case try XML.parse txt1 of
26253
0506197d285f message: proper root element for XML output;
wenzelm
parents: 26208
diff changeset
    93
        NONE => (txt1, Position.none)
26208
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
    94
      | SOME xml =>
26253
0506197d285f message: proper root element for XML output;
wenzelm
parents: 26208
diff changeset
    95
          (if print_mode_active full_markupN then XML.header ^ txt1 else XML.plain_content xml,
26208
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
    96
            the_default Position.none (get_pos xml)))
26527
c392354a1b79 Symbol.STX, Symbol.DEL;
wenzelm
parents: 26463
diff changeset
    97
      |>> translate_string (fn c => if c = Symbol.STX then Symbol.DEL else c);
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
    98
    val props =
26053
f8ee5cbb3068 tuned default position;
wenzelm
parents: 25849
diff changeset
    99
      Position.properties_of (Position.thread_data ())
f8ee5cbb3068 tuned default position;
wenzelm
parents: 25849
diff changeset
   100
      |> Position.default_properties pos;
25849
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   101
  in Output.writeln_default (special ch ^ print_props props ^ txt ^ special_end) end;
25554
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
fun init_message () =
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   104
  let
25849
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   105
    val pid = ("pid", string_of_pid (Posix.ProcEnv.getpid ()));
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   106
    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
   107
    val welcome = Session.welcome ();
25849
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   108
  in Output.writeln_default (special "H" ^ print_props [pid, session] ^ welcome ^ special_end) 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 () =
25849
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   116
 (Output.writeln_fn  := message "A";
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   117
  Output.priority_fn := message "B";
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   118
  Output.tracing_fn  := message "C";
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   119
  Output.warning_fn  := message "D";
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   120
  Output.error_fn    := message "E";
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   121
  Output.debug_fn    := message "F";
e80056f00b07 removed obsolete prompt and channel markups;
wenzelm
parents: 25842
diff changeset
   122
  Output.prompt_fn   := message "G");
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   123
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   124
26208
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   125
(* token translations *)
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
local
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   128
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   129
fun markup kind x =
26543
cd01c8eb314a moved output_markup to xml.ML;
wenzelm
parents: 26527
diff changeset
   130
  ((XML.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
   131
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   132
fun free_or_skolem x =
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   133
  (case try Name.dest_skolem x of
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   134
    NONE => markup Markup.freeN x
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   135
  | SOME x' => markup Markup.skolemN x');
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   136
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   137
fun var_or_skolem s =
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   138
  (case Lexicon.read_variable s of
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   139
    SOME (x, i) =>
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   140
      (case try Name.dest_skolem x of
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   141
        NONE => markup Markup.varN s
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   142
      | SOME x' => markup Markup.skolemN
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   143
          (setmp show_question_marks true Term.string_of_vname (x', i)))
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   144
  | NONE => markup Markup.varN s);
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   145
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   146
val token_trans =
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   147
 Syntax.tokentrans_mode full_markupN
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   148
  [("class", markup Markup.classN),
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   149
   ("tfree", markup Markup.tfreeN),
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   150
   ("tvar", markup Markup.tvarN),
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   151
   ("free", free_or_skolem),
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   152
   ("bound", markup Markup.boundN),
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   153
   ("var", var_or_skolem)];
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   154
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   155
in
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   156
26463
9283b4185fdf Context.>> : operate on Context.generic;
wenzelm
parents: 26435
diff changeset
   157
val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans));
26208
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   158
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   159
end;
278f47ae70d1 renamed test_markup to output_markup;
wenzelm
parents: 26053
diff changeset
   160
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   161
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
   162
(* init *)
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
   163
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
   164
fun init () =
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   165
 (change print_mode (update (op =) isabelle_processN);
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
   166
  setup_channels ();
25841
af7566faaa0f added symbol output mode, with XML escapes;
wenzelm
parents: 25820
diff changeset
   167
  init_message ();
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
   168
  Isar.secure_main ());
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
   169
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
   170
end;
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
   171