src/Pure/System/isabelle_process.ML
author wenzelm
Thu Dec 17 15:09:07 2009 +0100 (2009-12-17 ago)
changeset 34096 e438a5875c16
parent 33225 0496565527bd
child 34206 c29264a16ad8
permissions -rw-r--r--
simplified message format: chunks with explicit size in bytes;
robust message header via YXML.binary_text;
standard_message: refer to thread position only;
discontinued obsolete "-" output stream;
tuned;
wenzelm@30173
     1
(*  Title:      Pure/System/isabelle_process.ML
wenzelm@25528
     2
    Author:     Makarius
wenzelm@25528
     3
wenzelm@34096
     4
Isabelle process wrapper.
wenzelm@25631
     5
wenzelm@25631
     6
General format of process output:
wenzelm@34096
     7
  (1) message = "\002"  header chunk  body chunk
wenzelm@34096
     8
  (2) chunk = size (ASCII digits)  \n  content (YXML)
wenzelm@25528
     9
*)
wenzelm@25528
    10
wenzelm@25528
    11
signature ISABELLE_PROCESS =
wenzelm@25528
    12
sig
wenzelm@26574
    13
  val isabelle_processN: string
wenzelm@28044
    14
  val init: string -> unit
wenzelm@25528
    15
end;
wenzelm@25528
    16
wenzelm@31797
    17
structure Isabelle_Process: ISABELLE_PROCESS =
wenzelm@25528
    18
struct
wenzelm@25528
    19
wenzelm@26550
    20
(* print modes *)
wenzelm@25554
    21
wenzelm@25748
    22
val isabelle_processN = "isabelle_process";
wenzelm@25748
    23
wenzelm@26550
    24
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
wenzelm@28036
    25
val _ = Markup.add_mode isabelle_processN YXML.output_markup;
wenzelm@25841
    26
wenzelm@25841
    27
wenzelm@25841
    28
(* message markup *)
wenzelm@25841
    29
wenzelm@25841
    30
local
wenzelm@25810
    31
wenzelm@34096
    32
fun chunk s = string_of_int (size s) ^ "\n" ^ s;
wenzelm@26574
    33
wenzelm@34096
    34
fun message _ _ _ "" = ()
wenzelm@34096
    35
  | message out_stream ch props body =
wenzelm@34096
    36
      let
wenzelm@34096
    37
        val header = YXML.string_of (XML.Elem (ch, map (pairself YXML.binary_text) props, []));
wenzelm@34096
    38
        val msg = Symbol.STX ^ chunk header ^ chunk body;
wenzelm@34096
    39
      in TextIO.output (out_stream, msg) (*atomic output*) end;
wenzelm@25554
    40
wenzelm@25554
    41
in
wenzelm@25554
    42
wenzelm@34096
    43
fun standard_message out_stream ch body =
wenzelm@34096
    44
  message out_stream ch (Position.properties_of (Position.thread_data ())) body;
wenzelm@25554
    45
wenzelm@28044
    46
fun init_message out_stream =
wenzelm@25841
    47
  let
wenzelm@28491
    48
    val pid = (Markup.pidN, process_id ());
wenzelm@27972
    49
    val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
wenzelm@29522
    50
    val text = Session.welcome ();
wenzelm@34096
    51
  in message out_stream "A" [pid, session] text end;
wenzelm@25748
    52
wenzelm@25554
    53
end;
wenzelm@25554
    54
wenzelm@25554
    55
wenzelm@25841
    56
(* channels *)
wenzelm@25841
    57
wenzelm@28188
    58
local
wenzelm@28188
    59
wenzelm@28188
    60
fun auto_flush stream =
wenzelm@28188
    61
  let
wenzelm@28189
    62
    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
wenzelm@28188
    63
    fun loop () =
wenzelm@28188
    64
      (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
wenzelm@28188
    65
  in loop end;
wenzelm@28188
    66
wenzelm@28188
    67
in
wenzelm@28188
    68
wenzelm@28044
    69
fun setup_channels out =
wenzelm@28189
    70
  let
wenzelm@34096
    71
    val path = File.platform_path (Path.explode out);
wenzelm@34096
    72
    val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
wenzelm@34096
    73
    val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
wenzelm@28242
    74
    val _ = SimpleThread.fork false (auto_flush out_stream);
wenzelm@34096
    75
    val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
wenzelm@28242
    76
    val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
wenzelm@28044
    77
  in
wenzelm@34096
    78
    Output.status_fn   := standard_message out_stream "B";
wenzelm@34096
    79
    Output.writeln_fn  := standard_message out_stream "C";
wenzelm@34096
    80
    Output.priority_fn := standard_message out_stream "D";
wenzelm@34096
    81
    Output.tracing_fn  := standard_message out_stream "E";
wenzelm@34096
    82
    Output.warning_fn  := standard_message out_stream "F";
wenzelm@34096
    83
    Output.error_fn    := standard_message out_stream "G";
wenzelm@34096
    84
    Output.debug_fn    := standard_message out_stream "H";
wenzelm@28498
    85
    Output.prompt_fn   := ignore;
wenzelm@28044
    86
    out_stream
wenzelm@28044
    87
  end;
wenzelm@25841
    88
wenzelm@28188
    89
end;
wenzelm@28188
    90
wenzelm@25841
    91
wenzelm@25554
    92
(* init *)
wenzelm@25554
    93
wenzelm@28044
    94
fun init out =
wenzelm@32738
    95
 (Unsynchronized.change print_mode (update (op =) isabelle_processN);
wenzelm@28044
    96
  setup_channels out |> init_message;
wenzelm@28342
    97
  OuterKeyword.report ();
wenzelm@32793
    98
  Isar_Document.init ();
wenzelm@31384
    99
  Output.status (Markup.markup Markup.ready "");
wenzelm@26643
   100
  Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
wenzelm@25528
   101
wenzelm@25528
   102
end;