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