# HG changeset patch
# User wenzelm
# Date 1753875892 -7200
# Node ID 2b7080493211950ba2051c94a482396a72f31dc8
# Parent  499dd5d0d50f94d591a3473b702462da8fb5fade
more accurate output, based on persistent "command_range" markup;

diff -r 499dd5d0d50f -r 2b7080493211 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Jul 29 22:45:09 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Jul 30 13:44:52 2025 +0200
@@ -597,6 +597,15 @@
         case None => false
       }
 
+    def loaded_theory_command: Option[Command] =
+      if (node.commands.size == 1) {
+        node.commands.get_after(None) match {
+          case some@Some(command) if command.span.is_theory => some
+          case _ => None
+        }
+      }
+      else None
+
 
     /* pending edits */
 
diff -r 499dd5d0d50f -r 2b7080493211 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Tue Jul 29 22:45:09 2025 +0200
+++ b/src/Pure/PIDE/editor.scala	Wed Jul 30 13:44:52 2025 +0200
@@ -115,15 +115,30 @@
   ): Editor.Output = {
     if (snapshot.is_outdated) Editor.Output.none
     else {
-      snapshot.current_command(snapshot.node_name, offset) match {
+      val thy_command = snapshot.loaded_theory_command
+      val thy_command_range: Option[Text.Range] =
+        if (thy_command.isDefined) {
+          snapshot.command_range(Text.Range(offset)) orElse Some(Text.Range.offside)
+        }
+        else None
+
+      def filter(msg: XML.Elem): Boolean =
+        (for {
+          command_range <- thy_command_range
+          range <- Position.Range.unapply(msg.markup.properties)
+        } yield command_range.contains(range)) getOrElse true
+
+      thy_command orElse snapshot.current_command(snapshot.node_name, offset) match {
         case None => Editor.Output.init
         case Some(command) =>
-          if (restriction.isEmpty || restriction.get.contains(command)) {
+          if (thy_command.isDefined || restriction.isEmpty || restriction.get.contains(command)) {
             val results = snapshot.command_results(command)
             val messages = {
-              val (states, other) =
-                results.iterator.map(_._2).filterNot(Protocol.is_result).toList
-                  .partition(Protocol.is_state)
+              val (states, other) = {
+                List.from(
+                  for ((_, msg) <- results.iterator if !Protocol.is_result(msg) && filter(msg))
+                    yield msg).partition(Protocol.is_state)
+              }
               val (urgent, regular) = other.partition(Protocol.is_urgent)
               urgent ::: (if (output_state()) states else Nil) ::: regular
             }