# HG changeset patch
# User wenzelm
# Date 1199379044 -3600
# Node ID bac99880fa9966b30161312c3f81835f96fcdf16
# Parent  decb98ff92dd581e6ef58b75953132087a49133a
output message properties: id or position;

diff -r decb98ff92dd -r bac99880fa99 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Thu Jan 03 17:50:43 2008 +0100
+++ b/src/Pure/Tools/isabelle_process.ML	Thu Jan 03 17:50:44 2008 +0100
@@ -13,8 +13,12 @@
   startup on a separate line, e.g. "\nPID=4711\n"
 
   (c) properly marked-up messages, e.g. for writeln channel
-  "\002A" ^ text ^ "\002.\n" where the body text may consist of several
-  lines (output should be processed in one piece).
+
+  "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
+
+  where the props consist of name=value lines terminated by "\002,"
+  each, and the remaining text is any number of lines (output is
+  supposed to be processed in one piece).
 *)
 
 signature ISABELLE_PROCESS =
@@ -46,10 +50,20 @@
 local
 
 fun special c = chr 2 ^ c;
+val special_sep = special ",";
 val special_end = special ".";
 
-fun output c m s =
-  Output.writeln_default (special c ^ Markup.enclose m s ^ special_end);
+fun message_props () =
+  let
+    val thread_props = Toplevel.thread_properties ();
+    val props =
+      (case AList.lookup (op =) thread_props Markup.idN of
+        SOME id => [(Markup.idN, id)]
+      | NONE => Position.properties_of (#1 (Position.of_properties thread_props)));
+  in implode (map (fn (x, y) => x ^ "=" ^ y ^ special_sep ^ "\n") props) end;
+
+fun output ch markup txt =
+  Output.writeln_default (special ch ^ message_props () ^ Markup.enclose markup txt ^ special_end);
 
 in