src/Pure/Tools/isabelle_process.ML
author wenzelm
Thu, 03 Jan 2008 22:25:16 +0100
changeset 25820 8228b198c49e
parent 25810 bac99880fa99
child 25841 af7566faaa0f
permissions -rw-r--r--
simplified position_props, always include line/file fields;
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
9036ccd685b4 added output protocol specification;
wenzelm
parents: 25576
diff changeset
    12
  (b) echo of my pid on stdout, appears *relatively* early after
9036ccd685b4 added output protocol specification;
wenzelm
parents: 25576
diff changeset
    13
  startup on a separate line, e.g. "\nPID=4711\n"
9036ccd685b4 added output protocol specification;
wenzelm
parents: 25576
diff changeset
    14
9036ccd685b4 added output protocol specification;
wenzelm
parents: 25576
diff changeset
    15
  (c) properly marked-up messages, e.g. for writeln channel
25810
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    16
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    17
  "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    18
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    19
  where the props consist of name=value lines terminated by "\002,"
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    20
  each, and the remaining text is any number of lines (output is
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    21
  supposed to be processed in one piece).
25528
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
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    24
signature ISABELLE_PROCESS =
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    25
sig
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    26
  val test_markupN: string
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    27
  val test_markup: Markup.T -> output * output
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
25748
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    35
(* test_markup *)
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    36
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    37
val test_markupN = "test_markup";
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    38
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    39
fun test_markup (name, props) =
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    40
 (enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    41
  enclose "</" ">" name);
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    42
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    43
val _ = Markup.add_mode test_markupN test_markup;
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    44
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    45
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    46
(* channels *)
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    47
25748
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    48
val isabelle_processN = "isabelle_process";
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    49
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    50
local
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    51
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    52
fun special c = chr 2 ^ c;
25810
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    53
val special_sep = special ",";
25576
ee11881606b7 special_end: replaced Z by dot;
wenzelm
parents: 25565
diff changeset
    54
val special_end = special ".";
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    55
25820
8228b198c49e simplified position_props, always include line/file fields;
wenzelm
parents: 25810
diff changeset
    56
fun position_props () =
8228b198c49e simplified position_props, always include line/file fields;
wenzelm
parents: 25810
diff changeset
    57
  let val props = Position.properties_of (Position.thread_data ())
25810
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    58
  in implode (map (fn (x, y) => x ^ "=" ^ y ^ special_sep ^ "\n") props) end;
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    59
bac99880fa99 output message properties: id or position;
wenzelm
parents: 25748
diff changeset
    60
fun output ch markup txt =
25820
8228b198c49e simplified position_props, always include line/file fields;
wenzelm
parents: 25810
diff changeset
    61
  Output.writeln_default (special ch ^ position_props () ^ Markup.enclose markup txt ^ special_end);
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    62
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    63
in
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    64
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    65
fun setup_channels () =
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    66
 (Output.writeln_fn  := output "A" Markup.writeln;
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    67
  Output.priority_fn := output "B" Markup.priority;
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    68
  Output.tracing_fn  := output "C" Markup.tracing;
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    69
  Output.warning_fn  := output "D" Markup.warning;
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    70
  Output.error_fn    := output "E" Markup.error;
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    71
  Output.debug_fn    := output "F" Markup.debug);
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    72
25748
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    73
val _ = Markup.add_mode isabelle_processN (fn (name, _) =>
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    74
  if name = Markup.promptN then (special "G", special_end ^ "\n")
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    75
  else ("", ""));
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    76
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    77
end;
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    78
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    79
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    80
(* init *)
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    81
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    82
fun init () =
25631
9036ccd685b4 added output protocol specification;
wenzelm
parents: 25576
diff changeset
    83
 (Output.writeln_default ("\nPID=" ^ string_of_pid (Posix.ProcEnv.getpid ()));
25554
082d97057e23 added test_markup;
wenzelm
parents: 25528
diff changeset
    84
  setup_channels ();
25748
55a458a31e37 added PROMPT message;
wenzelm
parents: 25631
diff changeset
    85
  change print_mode (update (op =) isabelle_processN);
25528
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    86
  Isar.secure_main ());
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    87
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    88
end;
e67230c2b952 Isabelle process wrapper -- interaction via external program.
wenzelm
parents:
diff changeset
    89