more frugal standard message properties;
authorwenzelm
Tue, 12 Aug 2014 16:10:59 +0200
changeset 57913 8544ef75d1d8
parent 57912 dd9550f84106
child 57914 cbc55e5091a1
more frugal standard message properties;
src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Aug 12 15:46:20 2014 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Aug 12 16:10:59 2014 +0200
@@ -108,8 +108,12 @@
     fun standard_message props name body =
       if forall (fn s => s = "") body then ()
       else
-        message name
-          (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
+        let
+          val props' =
+            (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
+              (false, SOME id') => props @ [(Markup.idN, id')]
+            | _ => props);
+        in message name props' body end;
   in
     Output.status_fn := standard_message [] Markup.statusN;
     Output.report_fn := standard_message [] Markup.reportN;