non-critical output -- ship message in one piece;
authorwenzelm
Tue Oct 27 13:34:37 2009 +0100 (2009-10-27 ago)
changeset 332250496565527bd
parent 33224 e15ce5aeb6d5
child 33226 9a2911232c1b
non-critical output -- ship message in one piece;
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/System/isabelle_process.ML	Tue Oct 27 13:24:40 2009 +0100
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Oct 27 13:34:37 2009 +0100
     1.3 @@ -61,9 +61,6 @@
     1.4          else message_pos ts
     1.5      | _ => NONE);
     1.6  
     1.7 -fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
     1.8 -  (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
     1.9 -
    1.10  in
    1.11  
    1.12  fun message _ _ "" = ()
    1.13 @@ -74,14 +71,16 @@
    1.14            Position.properties_of (Position.thread_data ())
    1.15            |> Position.default_properties pos;
    1.16          val txt = clean_string [Symbol.STX] body;
    1.17 -      in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
    1.18 +        val msg = special ch ^ message_props props ^ txt ^ special_end ^ "\n";
    1.19 +      in TextIO.output (out_stream, msg) end;
    1.20  
    1.21  fun init_message out_stream =
    1.22    let
    1.23      val pid = (Markup.pidN, process_id ());
    1.24      val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
    1.25      val text = Session.welcome ();
    1.26 -  in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
    1.27 +    val msg = special "A" ^ message_props [pid, session] ^ text ^ special_end ^ "\n";
    1.28 +  in TextIO.output (out_stream, msg) end;
    1.29  
    1.30  end;
    1.31