more complete report positions, notably for command 'back' (amending eca176f773e0);

--- a/src/Pure/PIDE/command.scala	Wed Nov 25 15:24:55 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Nov 25 16:14:16 2020 +0100
@@ -345,13 +345,14 @@
               })
           }
 
-        case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
+        case XML.Elem(Markup(Markup.REPORT, atts0), msgs) =>
           (this /: msgs)((state, msg) =>
             {
               def bad(): Unit = Output.warning("Ignored report message: " + msg)
 
               msg match {
-                case XML.Elem(Markup(name, atts), args) =>
+                case XML.Elem(Markup(name, atts1), args) =>
+                  val atts = atts1 ::: atts0
                   command.reported_position(atts) match {
                     case Some((id, chunk_name)) =>
                       val target =

--- a/src/Pure/System/isabelle_process.ML	Wed Nov 25 15:24:55 2020 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Nov 25 16:14:16 2020 +0100
@@ -148,11 +148,10 @@
       if forall (fn s => s = "") ss then ()
       else
         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' (XML.blob ss) end;
+          val pos_props =
+            if exists Markup.position_property props then props
+            else props @ Position.properties_of (Position.thread_data ());
+        in message name pos_props (XML.blob ss) end;
 
     fun report_message ss =
       if Context_Position.pide_reports ()