src/Pure/System/isabelle_process.ML
author wenzelm
Thu Jun 25 13:25:35 2009 +0200 (2009-06-25 ago)
changeset 31797 203d5e61e3bc
parent 31384 ce169bd37fc0
child 32738 15bb09ca0378
permissions -rw-r--r--
renamed IsabelleProcess to Isabelle_Process;
renamed IsabelleSystem to Isabelle_System;
     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 fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
    65   (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
    66 
    67 in
    68 
    69 fun message _ _ "" = ()
    70   | message out_stream ch body =
    71       let
    72         val pos = the_default Position.none (message_pos (YXML.parse_body body));
    73         val props =
    74           Position.properties_of (Position.thread_data ())
    75           |> Position.default_properties pos;
    76         val txt = clean_string [Symbol.STX] body;
    77       in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
    78 
    79 fun init_message out_stream =
    80   let
    81     val pid = (Markup.pidN, process_id ());
    82     val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
    83     val text = Session.welcome ();
    84   in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
    85 
    86 end;
    87 
    88 
    89 (* channels *)
    90 
    91 local
    92 
    93 fun auto_flush stream =
    94   let
    95     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
    96     fun loop () =
    97       (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
    98   in loop end;
    99 
   100 in
   101 
   102 fun setup_channels out =
   103   let
   104     val out_stream =
   105       if out = "-" then TextIO.stdOut
   106       else
   107         let
   108           val path = File.platform_path (Path.explode out);
   109           val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
   110           val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
   111           val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
   112         in out_stream end;
   113     val _ = SimpleThread.fork false (auto_flush out_stream);
   114     val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
   115   in
   116     Output.status_fn   := message out_stream "B";
   117     Output.writeln_fn  := message out_stream "C";
   118     Output.priority_fn := message out_stream "D";
   119     Output.tracing_fn  := message out_stream "E";
   120     Output.warning_fn  := message out_stream "F";
   121     Output.error_fn    := message out_stream "G";
   122     Output.debug_fn    := message out_stream "H";
   123     Output.prompt_fn   := ignore;
   124     out_stream
   125   end;
   126 
   127 end;
   128 
   129 
   130 (* init *)
   131 
   132 fun init out =
   133  (change print_mode (update (op =) isabelle_processN);
   134   setup_channels out |> init_message;
   135   OuterKeyword.report ();
   136   Output.status (Markup.markup Markup.ready "");
   137   Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
   138 
   139 end;