# HG changeset patch
# User wenzelm
# Date 1199631477 -3600
# Node ID e80056f00b076dcd0deeb7caa825c621b30356f5
# Parent  fb998d0bf175b910e03080f1f9f47d4bea53f274
removed obsolete prompt and channel markups;
replaced prompt markup by prompt channel setup (avoids left-over XML encoding);
tuned;

diff -r fb998d0bf175 -r e80056f00b07 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Sun Jan 06 15:57:56 2008 +0100
+++ b/src/Pure/Tools/isabelle_process.ML	Sun Jan 06 15:57:57 2008 +0100
@@ -85,7 +85,10 @@
 
 in
 
-fun message ch markup raw_txt =
+val _ = Markup.add_mode isabelle_processN (fn (name, props) =>
+  if name = Markup.positionN then test_markup (name, props) else ("", ""));
+
+fun message ch raw_txt =
   let
     val (txt, pos) =
       (case try XML.tree_of_string (XML.element "message" [] [raw_txt]) of
@@ -96,16 +99,14 @@
       (case Position.properties_of (Position.thread_data ()) of
         [] => Position.properties_of pos
       | props => props);
-    val s = special ch ^ print_props props ^ Markup.enclose markup txt ^ special_end;
-  in Output.writeln_default s end;
+  in Output.writeln_default (special ch ^ print_props props ^ txt ^ special_end) end;
 
 fun init_message () =
   let
-    val pid = string_of_pid (Posix.ProcEnv.getpid ());
-    val session = List.last (Session.id ()) handle List.Empty => "unknown";
+    val pid = ("pid", string_of_pid (Posix.ProcEnv.getpid ()));
+    val session = ("session", List.last (Session.id ()) handle List.Empty => "unknown");
     val welcome = Session.welcome ();
-    val s = special "H" ^ print_props [("pid", pid), ("session", session)] ^ welcome ^ special_end;
-  in Output.writeln_default s end;
+  in Output.writeln_default (special "H" ^ print_props [pid, session] ^ welcome ^ special_end) end;
 
 end;
 
@@ -113,17 +114,14 @@
 (* channels *)
 
 fun setup_channels () =
- (Output.writeln_fn  := message "A" Markup.writeln;
-  Output.priority_fn := message "B" Markup.priority;
-  Output.tracing_fn  := message "C" Markup.tracing;
-  Output.warning_fn  := message "D" Markup.warning;
-  Output.error_fn    := message "E" Markup.error;
-  Output.debug_fn    := message "F" Markup.debug);
+ (Output.writeln_fn  := message "A";
+  Output.priority_fn := message "B";
+  Output.tracing_fn  := message "C";
+  Output.warning_fn  := message "D";
+  Output.error_fn    := message "E";
+  Output.debug_fn    := message "F";
+  Output.prompt_fn   := message "G");
 
-val _ = Markup.add_mode isabelle_processN (fn (name, props) =>
-  if name = Markup.promptN then (special "G", special_end ^ "\n")
-  else if name = Markup.positionN then test_markup (name, props)
-  else ("", ""));
 
 
 (* init *)