# HG changeset patch
# User wenzelm
# Date 1199395516 -3600
# Node ID 8228b198c49e8ff4529497cff9305f41502c00c3
# Parent  e6feb08b7f4b45f229b0a433bb59eba857559f36
simplified position_props, always include line/file fields;

diff -r e6feb08b7f4b -r 8228b198c49e src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Thu Jan 03 22:25:15 2008 +0100
+++ b/src/Pure/Tools/isabelle_process.ML	Thu Jan 03 22:25:16 2008 +0100
@@ -53,17 +53,12 @@
 val special_sep = special ",";
 val special_end = special ".";
 
-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)));
+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;
 
 fun output ch markup txt =
-  Output.writeln_default (special ch ^ message_props () ^ Markup.enclose markup txt ^ special_end);
+  Output.writeln_default (special ch ^ position_props () ^ Markup.enclose markup txt ^ special_end);
 
 in