src/Pure/Tools/isabelle_process.ML
author wenzelm
Thu Dec 06 00:21:34 2007 +0100 (2007-12-06 ago)
changeset 25554 082d97057e23
parent 25528 e67230c2b952
child 25565 33d30a53fae7
permissions -rw-r--r--
added test_markup;
added channel markup and specials;
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@25528
     6
*)
wenzelm@25528
     7
wenzelm@25528
     8
signature ISABELLE_PROCESS =
wenzelm@25528
     9
sig
wenzelm@25554
    10
  val test_markupN: string
wenzelm@25554
    11
  val test_markup: Markup.T -> output * output
wenzelm@25528
    12
  val init: unit -> unit
wenzelm@25528
    13
end;
wenzelm@25528
    14
wenzelm@25528
    15
structure IsabelleProcess: ISABELLE_PROCESS =
wenzelm@25528
    16
struct
wenzelm@25528
    17
wenzelm@25554
    18
(* test markup *)
wenzelm@25554
    19
wenzelm@25554
    20
val test_markupN = "test_markup";
wenzelm@25554
    21
wenzelm@25554
    22
fun test_markup (name, props) =
wenzelm@25554
    23
 (enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
wenzelm@25554
    24
  enclose "</" ">" name);
wenzelm@25554
    25
wenzelm@25554
    26
val _ = Markup.add_mode test_markupN test_markup;
wenzelm@25554
    27
wenzelm@25554
    28
wenzelm@25554
    29
(* channels *)
wenzelm@25554
    30
wenzelm@25554
    31
local
wenzelm@25554
    32
wenzelm@25554
    33
fun special c = chr 2 ^ c;
wenzelm@25554
    34
val special_end = special "Z";
wenzelm@25554
    35
wenzelm@25554
    36
fun output c m s =
wenzelm@25554
    37
  Output.writeln_default (special c ^ Markup.enclose m s ^ special_end);
wenzelm@25554
    38
wenzelm@25554
    39
in
wenzelm@25554
    40
wenzelm@25554
    41
fun setup_channels () =
wenzelm@25554
    42
 (Output.writeln_fn  := output "A" Markup.writeln;
wenzelm@25554
    43
  Output.priority_fn := output "B" Markup.priority;
wenzelm@25554
    44
  Output.tracing_fn  := output "C" Markup.tracing;
wenzelm@25554
    45
  Output.warning_fn  := output "D" Markup.warning;
wenzelm@25554
    46
  Output.error_fn    := output "E" Markup.error;
wenzelm@25554
    47
  Output.debug_fn    := output "F" Markup.debug);
wenzelm@25554
    48
wenzelm@25554
    49
end;
wenzelm@25554
    50
wenzelm@25554
    51
wenzelm@25554
    52
(* init *)
wenzelm@25554
    53
wenzelm@25528
    54
fun init () =
wenzelm@25554
    55
 (Output.writeln_default ("ML_PID=" ^ string_of_pid (Posix.ProcEnv.getpid ()));
wenzelm@25554
    56
  setup_channels ();
wenzelm@25528
    57
  Isar.secure_main ());
wenzelm@25528
    58
wenzelm@25528
    59
end;
wenzelm@25528
    60