src/Pure/Tools/isabelle_process.ML
author wenzelm
Thu Apr 03 21:23:42 2008 +0200 (2008-04-03 ago)
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;
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@25842
    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@25842
    18
  supposed to be processed in one piece);
wenzelm@25841
    19
wenzelm@25842
    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@26208
    25
  val full_markupN: string
wenzelm@25748
    26
  val isabelle_processN: string
wenzelm@25528
    27
  val init: unit -> unit
wenzelm@25528
    28
end;
wenzelm@25528
    29
wenzelm@25528
    30
structure IsabelleProcess: ISABELLE_PROCESS =
wenzelm@25528
    31
struct
wenzelm@25528
    32
wenzelm@26550
    33
(* print modes *)
wenzelm@25554
    34
wenzelm@25748
    35
val isabelle_processN = "isabelle_process";
wenzelm@26550
    36
val full_markupN = "full_markup";
wenzelm@25748
    37
wenzelm@26550
    38
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
wenzelm@25554
    39
wenzelm@26550
    40
val _ = Markup.add_mode isabelle_processN (fn (name, props) =>
wenzelm@26550
    41
  if print_mode_active full_markupN orelse name = Markup.positionN
wenzelm@26550
    42
  then YXML.output_markup (name, props) else ("", ""));
wenzelm@25841
    43
wenzelm@25841
    44
wenzelm@25841
    45
(* message markup *)
wenzelm@25841
    46
wenzelm@26527
    47
fun special ch = Symbol.STX ^ ch;
wenzelm@25810
    48
val special_sep = special ",";
wenzelm@25576
    49
val special_end = special ".";
wenzelm@25554
    50
wenzelm@25841
    51
local
wenzelm@25810
    52
wenzelm@26550
    53
fun message_props props =
wenzelm@25841
    54
  let
wenzelm@25841
    55
    val clean = translate_string (fn c =>
wenzelm@26527
    56
      if c = Symbol.STX orelse c = "\n" orelse c = "\r" then Symbol.DEL else c);
wenzelm@25841
    57
  in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
wenzelm@25841
    58
wenzelm@26550
    59
fun message_text ts =
wenzelm@26550
    60
  (if print_mode_active full_markupN
wenzelm@26550
    61
    then XML.header ^ XML.string_of (XML.Elem ("message", [], ts))
wenzelm@26550
    62
    else Buffer.content (fold XML.add_content ts Buffer.empty))
wenzelm@26550
    63
  |> translate_string (fn c => if c = Symbol.STX then Symbol.DEL else c);
wenzelm@26550
    64
wenzelm@26550
    65
fun message_pos ts = get_first get_pos ts
wenzelm@26550
    66
and get_pos (elem as XML.Elem (name, atts, ts)) =
wenzelm@25841
    67
      if name = Markup.positionN then SOME (Position.of_properties atts)
wenzelm@26550
    68
      else message_pos ts
wenzelm@26550
    69
  | get_pos _ = NONE
wenzelm@25554
    70
wenzelm@25554
    71
in
wenzelm@25554
    72
wenzelm@26550
    73
fun message ch body =
wenzelm@25841
    74
  let
wenzelm@25841
    75
    val (txt, pos) =
wenzelm@26550
    76
      let val ts = YXML.parse_body body
wenzelm@26550
    77
      in (message_text ts, the_default Position.none (message_pos ts)) end
wenzelm@26550
    78
      handle Fail msg => ("*** MALFORMED MESSAGE ***\n" ^ msg, Position.none);
wenzelm@25841
    79
    val props =
wenzelm@26053
    80
      Position.properties_of (Position.thread_data ())
wenzelm@26053
    81
      |> Position.default_properties pos;
wenzelm@26550
    82
  in Output.writeln_default (special ch ^ message_props props ^ txt ^ special_end) end;
wenzelm@25554
    83
wenzelm@25841
    84
fun init_message () =
wenzelm@25841
    85
  let
wenzelm@25849
    86
    val pid = ("pid", string_of_pid (Posix.ProcEnv.getpid ()));
wenzelm@25849
    87
    val session = ("session", List.last (Session.id ()) handle List.Empty => "unknown");
wenzelm@25841
    88
    val welcome = Session.welcome ();
wenzelm@26550
    89
  in Output.writeln_default (special "H" ^ message_props [pid, session] ^ welcome ^ special_end) end;
wenzelm@25748
    90
wenzelm@25554
    91
end;
wenzelm@25554
    92
wenzelm@25554
    93
wenzelm@25841
    94
(* channels *)
wenzelm@25841
    95
wenzelm@25841
    96
fun setup_channels () =
wenzelm@25849
    97
 (Output.writeln_fn  := message "A";
wenzelm@25849
    98
  Output.priority_fn := message "B";
wenzelm@25849
    99
  Output.tracing_fn  := message "C";
wenzelm@25849
   100
  Output.warning_fn  := message "D";
wenzelm@25849
   101
  Output.error_fn    := message "E";
wenzelm@25849
   102
  Output.debug_fn    := message "F";
wenzelm@25849
   103
  Output.prompt_fn   := message "G");
wenzelm@25841
   104
wenzelm@25841
   105
wenzelm@26208
   106
(* token translations *)
wenzelm@26208
   107
wenzelm@26208
   108
local
wenzelm@26208
   109
wenzelm@26208
   110
fun markup kind x =
wenzelm@26550
   111
  ((YXML.output_markup (kind, []) |-> enclose) (Output.output x), Symbol.length (Symbol.explode x));
wenzelm@26208
   112
wenzelm@26208
   113
fun free_or_skolem x =
wenzelm@26208
   114
  (case try Name.dest_skolem x of
wenzelm@26208
   115
    NONE => markup Markup.freeN x
wenzelm@26208
   116
  | SOME x' => markup Markup.skolemN x');
wenzelm@26208
   117
wenzelm@26208
   118
fun var_or_skolem s =
wenzelm@26208
   119
  (case Lexicon.read_variable s of
wenzelm@26208
   120
    SOME (x, i) =>
wenzelm@26208
   121
      (case try Name.dest_skolem x of
wenzelm@26208
   122
        NONE => markup Markup.varN s
wenzelm@26208
   123
      | SOME x' => markup Markup.skolemN
wenzelm@26208
   124
          (setmp show_question_marks true Term.string_of_vname (x', i)))
wenzelm@26208
   125
  | NONE => markup Markup.varN s);
wenzelm@26208
   126
wenzelm@26208
   127
val token_trans =
wenzelm@26208
   128
 Syntax.tokentrans_mode full_markupN
wenzelm@26208
   129
  [("class", markup Markup.classN),
wenzelm@26208
   130
   ("tfree", markup Markup.tfreeN),
wenzelm@26208
   131
   ("tvar", markup Markup.tvarN),
wenzelm@26208
   132
   ("free", free_or_skolem),
wenzelm@26208
   133
   ("bound", markup Markup.boundN),
wenzelm@26208
   134
   ("var", var_or_skolem)];
wenzelm@26208
   135
wenzelm@26208
   136
in
wenzelm@26208
   137
wenzelm@26463
   138
val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans));
wenzelm@26208
   139
wenzelm@26208
   140
end;
wenzelm@26208
   141
wenzelm@25841
   142
wenzelm@25554
   143
(* init *)
wenzelm@25554
   144
wenzelm@25528
   145
fun init () =
wenzelm@25841
   146
 (change print_mode (update (op =) isabelle_processN);
wenzelm@25554
   147
  setup_channels ();
wenzelm@25841
   148
  init_message ();
wenzelm@25528
   149
  Isar.secure_main ());
wenzelm@25528
   150
wenzelm@25528
   151
end;
wenzelm@25528
   152