src/Pure/System/isabelle_process.ML
author wenzelm
Tue Oct 27 13:34:37 2009 +0100 (2009-10-27 ago)
changeset 33225 0496565527bd
parent 32793 24ba50c14ec5
child 34096 e438a5875c16
permissions -rw-r--r--
non-critical output -- ship message in one piece;
     1 (*  Title:      Pure/System/isabelle_process.ML
     2     Author:     Makarius
     3 
     4 Isabelle process wrapper -- interaction via external program.
     5 
     6 General format of process output:
     7 
     8   (1) unmarked stdout/stderr, no line structure (output should be
     9   processed immediately as it arrives);
    10 
    11   (2) properly marked-up messages, e.g. for writeln channel
    12 
    13   "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
    14 
    15   where the props consist of name=value lines terminated by "\002,\n"
    16   each, and the remaining text is any number of lines (output is
    17   supposed to be processed in one piece);
    18 
    19   (3) special init message holds "pid" and "session" property;
    20 
    21   (4) message content is encoded in YXML format.
    22 *)
    23 
    24 signature ISABELLE_PROCESS =
    25 sig
    26   val isabelle_processN: string
    27   val init: string -> unit
    28 end;
    29 
    30 structure Isabelle_Process: ISABELLE_PROCESS =
    31 struct
    32 
    33 (* print modes *)
    34 
    35 val isabelle_processN = "isabelle_process";
    36 
    37 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
    38 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
    39 
    40 
    41 (* message markup *)
    42 
    43 fun special ch = Symbol.STX ^ ch;
    44 val special_sep = special ",";
    45 val special_end = special ".";
    46 
    47 local
    48 
    49 fun clean_string bad str =
    50   if exists_string (member (op =) bad) str then
    51     translate_string (fn c => if member (op =) bad c then Symbol.DEL else c) str
    52   else str;
    53 
    54 fun message_props props =
    55   let val clean = clean_string [Symbol.STX, "\n", "\r"]
    56   in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
    57 
    58 fun message_pos trees = trees |> get_first
    59   (fn XML.Elem (name, atts, ts) =>
    60         if name = Markup.positionN then SOME (Position.of_properties atts)
    61         else message_pos ts
    62     | _ => NONE);
    63 
    64 in
    65 
    66 fun message _ _ "" = ()
    67   | message out_stream ch body =
    68       let
    69         val pos = the_default Position.none (message_pos (YXML.parse_body body));
    70         val props =
    71           Position.properties_of (Position.thread_data ())
    72           |> Position.default_properties pos;
    73         val txt = clean_string [Symbol.STX] body;
    74         val msg = special ch ^ message_props props ^ txt ^ special_end ^ "\n";
    75       in TextIO.output (out_stream, msg) end;
    76 
    77 fun init_message out_stream =
    78   let
    79     val pid = (Markup.pidN, process_id ());
    80     val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
    81     val text = Session.welcome ();
    82     val msg = special "A" ^ message_props [pid, session] ^ text ^ special_end ^ "\n";
    83   in TextIO.output (out_stream, msg) end;
    84 
    85 end;
    86 
    87 
    88 (* channels *)
    89 
    90 local
    91 
    92 fun auto_flush stream =
    93   let
    94     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
    95     fun loop () =
    96       (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
    97   in loop end;
    98 
    99 in
   100 
   101 fun setup_channels out =
   102   let
   103     val out_stream =
   104       if out = "-" then TextIO.stdOut
   105       else
   106         let
   107           val path = File.platform_path (Path.explode out);
   108           val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
   109           val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
   110           val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
   111         in out_stream end;
   112     val _ = SimpleThread.fork false (auto_flush out_stream);
   113     val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
   114   in
   115     Output.status_fn   := message out_stream "B";
   116     Output.writeln_fn  := message out_stream "C";
   117     Output.priority_fn := message out_stream "D";
   118     Output.tracing_fn  := message out_stream "E";
   119     Output.warning_fn  := message out_stream "F";
   120     Output.error_fn    := message out_stream "G";
   121     Output.debug_fn    := message out_stream "H";
   122     Output.prompt_fn   := ignore;
   123     out_stream
   124   end;
   125 
   126 end;
   127 
   128 
   129 (* init *)
   130 
   131 fun init out =
   132  (Unsynchronized.change print_mode (update (op =) isabelle_processN);
   133   setup_channels out |> init_message;
   134   OuterKeyword.report ();
   135   Isar_Document.init ();
   136   Output.status (Markup.markup Markup.ready "");
   137   Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
   138 
   139 end;