# HG changeset patch
# User wenzelm
# Date 1407852659 -7200
# Node ID 8544ef75d1d862448ab37161c8410504ac0d0976
# Parent  dd9550f8410651520faf919c50a46b849b6c0e83
more frugal standard message properties;

diff -r dd9550f84106 -r 8544ef75d1d8 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;