src/Pure/System/isabelle_process.ML
author wenzelm
Sat Aug 07 21:03:06 2010 +0200 (2010-08-07 ago)
changeset 38228 ada3ab6b9085
parent 37687 e07dacec79e7
child 38236 d8c7be27e01d
permissions -rw-r--r--
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
     1 (*  Title:      Pure/System/isabelle_process.ML
     2     Author:     Makarius
     3 
     4 Isabelle process wrapper.
     5 
     6 General format of process output:
     7   (1) message = "\002"  header chunk  body chunk
     8   (2) chunk = size (ASCII digits)  \n  content (YXML)
     9 *)
    10 
    11 signature ISABELLE_PROCESS =
    12 sig
    13   val isabelle_processN: string
    14   val init: string -> unit
    15 end;
    16 
    17 structure Isabelle_Process: ISABELLE_PROCESS =
    18 struct
    19 
    20 (* print modes *)
    21 
    22 val isabelle_processN = "isabelle_process";
    23 
    24 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
    25 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
    26 
    27 
    28 (* message markup *)
    29 
    30 local
    31 
    32 fun chunk s = string_of_int (size s) ^ "\n" ^ s;
    33 
    34 fun message _ _ _ "" = ()
    35   | message out_stream ch props body =
    36       let
    37         val header = YXML.string_of (XML.Elem ((ch, map (pairself YXML.binary_text) props), []));
    38         val msg = Symbol.STX ^ chunk header ^ chunk body;
    39       in TextIO.output (out_stream, msg) (*atomic output*) end;
    40 
    41 in
    42 
    43 fun standard_message out_stream ch body =
    44   message out_stream ch (Position.properties_of (Position.thread_data ())) body;
    45 
    46 fun init_message out_stream =
    47   message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
    48 
    49 end;
    50 
    51 
    52 (* channels *)
    53 
    54 local
    55 
    56 fun auto_flush stream =
    57   let
    58     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
    59     fun loop () =
    60       (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
    61   in loop end;
    62 
    63 in
    64 
    65 fun setup_channels out =
    66   let
    67     val path = File.platform_path (Path.explode out);
    68     val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
    69     val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
    70     val _ = Simple_Thread.fork false (auto_flush out_stream);
    71     val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
    72     val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
    73   in
    74     Output.status_fn   := standard_message out_stream "B";
    75     Output.writeln_fn  := standard_message out_stream "C";
    76     Output.tracing_fn  := standard_message out_stream "D";
    77     Output.warning_fn  := standard_message out_stream "E";
    78     Output.error_fn    := standard_message out_stream "F";
    79     Output.debug_fn    := standard_message out_stream "G";
    80     Output.priority_fn := ! Output.writeln_fn;
    81     Output.prompt_fn   := ignore;
    82     out_stream
    83   end;
    84 
    85 end;
    86 
    87 
    88 (* init *)
    89 
    90 fun init out =
    91  (Unsynchronized.change print_mode
    92     (fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]);
    93   setup_channels out |> init_message;
    94   quick_and_dirty := true;  (* FIXME !? *)
    95   Keyword.report ();
    96   Output.status (Markup.markup Markup.ready "");
    97   Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
    98 
    99 end;