src/Pure/System/isabelle_process.ML
changeset 30173 eabece26b89b
parent 29522 793766d4c1b5
child 31384 ce169bd37fc0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Sat Feb 28 18:00:20 2009 +0100
     1.3 @@ -0,0 +1,138 @@
     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 +
     1.9 +General format of process output:
    1.10 +
    1.11 +  (1) unmarked stdout/stderr, no line structure (output should be
    1.12 +  processed immediately as it arrives);
    1.13 +
    1.14 +  (2) properly marked-up messages, e.g. for writeln channel
    1.15 +
    1.16 +  "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
    1.17 +
    1.18 +  where the props consist of name=value lines terminated by "\002,\n"
    1.19 +  each, and the remaining text is any number of lines (output is
    1.20 +  supposed to be processed in one piece);
    1.21 +
    1.22 +  (3) special init message holds "pid" and "session" property;
    1.23 +
    1.24 +  (4) message content is encoded in YXML format.
    1.25 +*)
    1.26 +
    1.27 +signature ISABELLE_PROCESS =
    1.28 +sig
    1.29 +  val isabelle_processN: string
    1.30 +  val init: string -> unit
    1.31 +end;
    1.32 +
    1.33 +structure IsabelleProcess: ISABELLE_PROCESS =
    1.34 +struct
    1.35 +
    1.36 +(* print modes *)
    1.37 +
    1.38 +val isabelle_processN = "isabelle_process";
    1.39 +
    1.40 +val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
    1.41 +val _ = Markup.add_mode isabelle_processN YXML.output_markup;
    1.42 +
    1.43 +
    1.44 +(* message markup *)
    1.45 +
    1.46 +fun special ch = Symbol.STX ^ ch;
    1.47 +val special_sep = special ",";
    1.48 +val special_end = special ".";
    1.49 +
    1.50 +local
    1.51 +
    1.52 +fun clean_string bad str =
    1.53 +  if exists_string (member (op =) bad) str then
    1.54 +    translate_string (fn c => if member (op =) bad c then Symbol.DEL else c) str
    1.55 +  else str;
    1.56 +
    1.57 +fun message_props props =
    1.58 +  let val clean = clean_string [Symbol.STX, "\n", "\r"]
    1.59 +  in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
    1.60 +
    1.61 +fun message_pos trees = trees |> get_first
    1.62 +  (fn XML.Elem (name, atts, ts) =>
    1.63 +        if name = Markup.positionN then SOME (Position.of_properties atts)
    1.64 +        else message_pos ts
    1.65 +    | _ => NONE);
    1.66 +
    1.67 +fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
    1.68 +  (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
    1.69 +
    1.70 +in
    1.71 +
    1.72 +fun message _ _ "" = ()
    1.73 +  | message out_stream ch body =
    1.74 +      let
    1.75 +        val pos = the_default Position.none (message_pos (YXML.parse_body body));
    1.76 +        val props =
    1.77 +          Position.properties_of (Position.thread_data ())
    1.78 +          |> Position.default_properties pos;
    1.79 +        val txt = clean_string [Symbol.STX] body;
    1.80 +      in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
    1.81 +
    1.82 +fun init_message out_stream =
    1.83 +  let
    1.84 +    val pid = (Markup.pidN, process_id ());
    1.85 +    val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
    1.86 +    val text = Session.welcome ();
    1.87 +  in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
    1.88 +
    1.89 +end;
    1.90 +
    1.91 +
    1.92 +(* channels *)
    1.93 +
    1.94 +local
    1.95 +
    1.96 +fun auto_flush stream =
    1.97 +  let
    1.98 +    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
    1.99 +    fun loop () =
   1.100 +      (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
   1.101 +  in loop end;
   1.102 +
   1.103 +in
   1.104 +
   1.105 +fun setup_channels out =
   1.106 +  let
   1.107 +    val out_stream =
   1.108 +      if out = "-" then TextIO.stdOut
   1.109 +      else
   1.110 +        let
   1.111 +          val path = File.platform_path (Path.explode out);
   1.112 +          val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
   1.113 +          val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
   1.114 +          val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
   1.115 +        in out_stream end;
   1.116 +    val _ = SimpleThread.fork false (auto_flush out_stream);
   1.117 +    val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
   1.118 +  in
   1.119 +    Output.status_fn   := message out_stream "B";
   1.120 +    Output.writeln_fn  := message out_stream "C";
   1.121 +    Output.priority_fn := message out_stream "D";
   1.122 +    Output.tracing_fn  := message out_stream "E";
   1.123 +    Output.warning_fn  := message out_stream "F";
   1.124 +    Output.error_fn    := message out_stream "G";
   1.125 +    Output.debug_fn    := message out_stream "H";
   1.126 +    Output.prompt_fn   := ignore;
   1.127 +    out_stream
   1.128 +  end;
   1.129 +
   1.130 +end;
   1.131 +
   1.132 +
   1.133 +(* init *)
   1.134 +
   1.135 +fun init out =
   1.136 + (change print_mode (update (op =) isabelle_processN);
   1.137 +  setup_channels out |> init_message;
   1.138 +  OuterKeyword.report ();
   1.139 +  Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
   1.140 +
   1.141 +end;