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