src/Pure/Tools/isabelle_process.ML

 General format of process output:
 
   (a) unmarked stdout/stderr, no line structure (output should be
   processed immediately as it arrives)
 
-  (b) echo of my pid on stdout, appears *relatively* early after
-  startup on a separate line, e.g. "\nPID=4711\n"
-
-  (c) properly marked-up messages, e.g. for writeln channel
+  (b) properly marked-up messages, e.g. for writeln channel
 
   "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
 
-  where the props consist of name=value lines terminated by "\002,"
+  where the props consist of name=value lines terminated by "\002,\n"
   each, and the remaining text is any number of lines (output is
   supposed to be processed in one piece).
+
+  (c) Special init message holds "pid" and "session" property.
 *)
 
 signature ISABELLE_PROCESS =
 sig
   val test_markupN: string

   enclose "</" ">" name);
 
 val _ = Markup.add_mode test_markupN test_markup;
 
 
-(* channels *)
+(* symbol output *)
 
 val isabelle_processN = "isabelle_process";
 
 local
 
-fun special c = chr 2 ^ c;
+fun output str =
+  let
+    fun out s = if Symbol.is_raw s then Symbol.decode_raw s else XML.text s;
+    val syms = Symbol.explode str;
+  in (implode (map out syms), Symbol.length syms) end;
+
+in
+
+val _ = Output.add_mode isabelle_processN output Symbol.encode_raw;
+
+end;
+
+
+(* message markup *)
+
+val STX = chr 2;
+val DEL = chr 127;
+
+fun special ch = STX ^ ch;
 val special_sep = special ",";
 val special_end = special ".";
 
-fun position_props () =
-  let val props = Position.properties_of (Position.thread_data ())
-  in implode (map (fn (x, y) => x ^ "=" ^ y ^ special_sep ^ "\n") props) end;
+local
 
-fun output ch markup txt =
-  Output.writeln_default (special ch ^ position_props () ^ Markup.enclose markup txt ^ special_end);
+fun print_props props =
+  let
+    val clean = translate_string (fn c =>
+      if c = STX orelse c = "\n" orelse c = "\r" then DEL else c);
+  in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
+
+fun get_pos (elem as XML.Elem (name, atts, ts)) =
+      if name = Markup.positionN then SOME (Position.of_properties atts)
+      else get_first get_pos ts
+  | get_pos _ = NONE;
 
 in
 
-fun setup_channels () =
- (Output.writeln_fn  := output "A" Markup.writeln;
-  Output.priority_fn := output "B" Markup.priority;
-  Output.tracing_fn  := output "C" Markup.tracing;
-  Output.warning_fn  := output "D" Markup.warning;
-  Output.error_fn    := output "E" Markup.error;
-  Output.debug_fn    := output "F" Markup.debug);
+fun message ch markup raw_txt =
+  let
+    val (txt, pos) =
+      (case try XML.tree_of_string (XML.element "message" [] [raw_txt]) of
+        NONE => (raw_txt, Position.none)
+      | SOME xml => (XML.plain_content xml, the_default Position.none (get_pos xml)))
+      |>> translate_string (fn c => if c = STX then DEL else c);
+    val props =
+      (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;
 
-val _ = Markup.add_mode isabelle_processN (fn (name, _) =>
-  if name = Markup.promptN then (special "G", special_end ^ "\n")
-  else ("", ""));
+fun init_message () =
+  let
+    val pid = string_of_pid (Posix.ProcEnv.getpid ());
+    val 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;
 
 end;
+
+
+(* 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);
+
+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 *)
 
 fun init () =
- (Output.writeln_default ("\nPID=" ^ string_of_pid (Posix.ProcEnv.getpid ()));
+ (change print_mode (update (op =) isabelle_processN);
   setup_channels ();
-  change print_mode (update (op =) isabelle_processN);
+  init_message ();
   Isar.secure_main ());
 
 end;