src/Pure/System/isabelle_process.ML
changeset 34096 e438a5875c16
parent 33225 0496565527bd
child 34206 c29264a16ad8
     1.1 --- a/src/Pure/System/isabelle_process.ML	Thu Dec 17 13:58:15 2009 +0100
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Dec 17 15:09:07 2009 +0100
     1.3 @@ -1,24 +1,11 @@
     1.4  (*  Title:      Pure/System/isabelle_process.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -Isabelle process wrapper -- interaction via external program.
     1.8 +Isabelle process wrapper.
     1.9  
    1.10  General format of process output:
    1.11 -
    1.12 -  (1) unmarked stdout/stderr, no line structure (output should be
    1.13 -  processed immediately as it arrives);
    1.14 -
    1.15 -  (2) properly marked-up messages, e.g. for writeln channel
    1.16 -
    1.17 -  "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
    1.18 -
    1.19 -  where the props consist of name=value lines terminated by "\002,\n"
    1.20 -  each, and the remaining text is any number of lines (output is
    1.21 -  supposed to be processed in one piece);
    1.22 -
    1.23 -  (3) special init message holds "pid" and "session" property;
    1.24 -
    1.25 -  (4) message content is encoded in YXML format.
    1.26 +  (1) message = "\002"  header chunk  body chunk
    1.27 +  (2) chunk = size (ASCII digits)  \n  content (YXML)
    1.28  *)
    1.29  
    1.30  signature ISABELLE_PROCESS =
    1.31 @@ -40,47 +27,28 @@
    1.32  
    1.33  (* message markup *)
    1.34  
    1.35 -fun special ch = Symbol.STX ^ ch;
    1.36 -val special_sep = special ",";
    1.37 -val special_end = special ".";
    1.38 -
    1.39  local
    1.40  
    1.41 -fun clean_string bad str =
    1.42 -  if exists_string (member (op =) bad) str then
    1.43 -    translate_string (fn c => if member (op =) bad c then Symbol.DEL else c) str
    1.44 -  else str;
    1.45 +fun chunk s = string_of_int (size s) ^ "\n" ^ s;
    1.46  
    1.47 -fun message_props props =
    1.48 -  let val clean = clean_string [Symbol.STX, "\n", "\r"]
    1.49 -  in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
    1.50 -
    1.51 -fun message_pos trees = trees |> get_first
    1.52 -  (fn XML.Elem (name, atts, ts) =>
    1.53 -        if name = Markup.positionN then SOME (Position.of_properties atts)
    1.54 -        else message_pos ts
    1.55 -    | _ => NONE);
    1.56 +fun message _ _ _ "" = ()
    1.57 +  | message out_stream ch props body =
    1.58 +      let
    1.59 +        val header = YXML.string_of (XML.Elem (ch, map (pairself YXML.binary_text) props, []));
    1.60 +        val msg = Symbol.STX ^ chunk header ^ chunk body;
    1.61 +      in TextIO.output (out_stream, msg) (*atomic output*) end;
    1.62  
    1.63  in
    1.64  
    1.65 -fun message _ _ "" = ()
    1.66 -  | message out_stream ch body =
    1.67 -      let
    1.68 -        val pos = the_default Position.none (message_pos (YXML.parse_body body));
    1.69 -        val props =
    1.70 -          Position.properties_of (Position.thread_data ())
    1.71 -          |> Position.default_properties pos;
    1.72 -        val txt = clean_string [Symbol.STX] body;
    1.73 -        val msg = special ch ^ message_props props ^ txt ^ special_end ^ "\n";
    1.74 -      in TextIO.output (out_stream, msg) end;
    1.75 +fun standard_message out_stream ch body =
    1.76 +  message out_stream ch (Position.properties_of (Position.thread_data ())) body;
    1.77  
    1.78  fun init_message out_stream =
    1.79    let
    1.80      val pid = (Markup.pidN, process_id ());
    1.81      val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
    1.82      val text = Session.welcome ();
    1.83 -    val msg = special "A" ^ message_props [pid, session] ^ text ^ special_end ^ "\n";
    1.84 -  in TextIO.output (out_stream, msg) end;
    1.85 +  in message out_stream "A" [pid, session] text end;
    1.86  
    1.87  end;
    1.88  
    1.89 @@ -100,25 +68,20 @@
    1.90  
    1.91  fun setup_channels out =
    1.92    let
    1.93 -    val out_stream =
    1.94 -      if out = "-" then TextIO.stdOut
    1.95 -      else
    1.96 -        let
    1.97 -          val path = File.platform_path (Path.explode out);
    1.98 -          val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
    1.99 -          val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
   1.100 -          val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
   1.101 -        in out_stream end;
   1.102 +    val path = File.platform_path (Path.explode out);
   1.103 +    val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
   1.104 +    val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
   1.105      val _ = SimpleThread.fork false (auto_flush out_stream);
   1.106 +    val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
   1.107      val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
   1.108    in
   1.109 -    Output.status_fn   := message out_stream "B";
   1.110 -    Output.writeln_fn  := message out_stream "C";
   1.111 -    Output.priority_fn := message out_stream "D";
   1.112 -    Output.tracing_fn  := message out_stream "E";
   1.113 -    Output.warning_fn  := message out_stream "F";
   1.114 -    Output.error_fn    := message out_stream "G";
   1.115 -    Output.debug_fn    := message out_stream "H";
   1.116 +    Output.status_fn   := standard_message out_stream "B";
   1.117 +    Output.writeln_fn  := standard_message out_stream "C";
   1.118 +    Output.priority_fn := standard_message out_stream "D";
   1.119 +    Output.tracing_fn  := standard_message out_stream "E";
   1.120 +    Output.warning_fn  := standard_message out_stream "F";
   1.121 +    Output.error_fn    := standard_message out_stream "G";
   1.122 +    Output.debug_fn    := standard_message out_stream "H";
   1.123      Output.prompt_fn   := ignore;
   1.124      out_stream
   1.125    end;