# HG changeset patch
# User wenzelm
# Date 1754307281 -7200
# Node ID 962b73cc57dc94cc9079bcd330b11bcd42e6da2f
# Parent  634b8a0f296659ae35997a08761d86cbb7b232d0
clarified signature: more self-contained operation;

diff -r 634b8a0f2966 -r 962b73cc57dc src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Aug 03 16:58:04 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Aug 04 13:34:41 2025 +0200
@@ -597,10 +597,11 @@
         case None => false
       }
 
-    def loaded_theory_command: Option[Command] =
-      if (node.commands.size == 1) {
+    def loaded_theory_command(caret_offset: Text.Offset): Option[(Command, Text.Range)] =
+      if (node_name.is_theory) {
         node.commands.get_after(None) match {
-          case some@Some(command) if command.span.is_theory => some
+          case Some(command) if command.span.is_theory =>
+            Some(command -> command_range(Text.Range(caret_offset)).getOrElse(Text.Range.offside))
           case _ => None
         }
       }
diff -r 634b8a0f2966 -r 962b73cc57dc src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Sun Aug 03 16:58:04 2025 +0200
+++ b/src/Pure/PIDE/editor.scala	Mon Aug 04 13:34:41 2025 +0200
@@ -110,26 +110,22 @@
 
   def output(
     snapshot: Document.Snapshot,
-    offset: Text.Offset,
+    caret_offset: Text.Offset,
     restriction: Option[Set[Command]] = None
   ): Editor.Output = {
     if (snapshot.is_outdated) Editor.Output.none
     else {
-      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
+      val thy_command_range = snapshot.loaded_theory_command(caret_offset)
+      val thy_command = thy_command_range.map(_._1)
 
       def filter(msg: XML.Elem): Boolean =
         (for {
-          command_range <- thy_command_range
+          (command, command_range) <- thy_command_range
           msg_range <- Position.Range.unapply(msg.markup.properties)
-          chunk_range <- thy_command.get.chunk.incorporate(msg_range)
+          chunk_range <- command.chunk.incorporate(msg_range)
         } yield command_range.contains(chunk_range)) getOrElse true
 
-      thy_command orElse snapshot.current_command(snapshot.node_name, offset) match {
+      thy_command orElse snapshot.current_command(snapshot.node_name, caret_offset) match {
         case None => Editor.Output.init
         case Some(command) =>
           if (thy_command.isDefined || restriction.isEmpty || restriction.get.contains(command)) {
diff -r 634b8a0f2966 -r 962b73cc57dc src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Sun Aug 03 16:58:04 2025 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Mon Aug 04 13:34:41 2025 +0200
@@ -579,7 +579,7 @@
 
     def current_command(snapshot: Document.Snapshot): Option[Command] = {
       resources.get_caret() match {
-        case Some(caret) if snapshot.loaded_theory_command.isEmpty =>
+        case Some(caret) if snapshot.loaded_theory_command(caret.offset).isEmpty =>
           snapshot.current_command(caret.node_name, caret.offset)
         case _ => None
       }
diff -r 634b8a0f2966 -r 962b73cc57dc src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Aug 03 16:58:04 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 04 13:34:41 2025 +0200
@@ -81,9 +81,10 @@
   override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
     GUI_Thread.require {
       val text_area = view.getTextArea
+      val caret_offset = text_area.getCaretPosition
       Document_View.get(text_area) match {
-        case Some(doc_view) if snapshot.loaded_theory_command.isEmpty =>
-          snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition)
+        case Some(doc_view) if snapshot.loaded_theory_command(caret_offset).isEmpty =>
+          snapshot.current_command(doc_view.model.node_name, caret_offset)
         case _ => None
       }
     }
diff -r 634b8a0f2966 -r 962b73cc57dc src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sun Aug 03 16:58:04 2025 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Aug 04 13:34:41 2025 +0200
@@ -37,9 +37,9 @@
 
   private def handle_update(restriction: Option[Set[Command]] = None): Unit =
     GUI_Thread.require {
-      val offset = view.getTextArea.getCaretPosition
+      val caret_offset = view.getTextArea.getCaretPosition
       for (snapshot <- PIDE.editor.current_node_snapshot(view)) {
-        val output = PIDE.editor.output(snapshot, offset, restriction = restriction)
+        val output = PIDE.editor.output(snapshot, caret_offset, restriction = restriction)
         if (output.defined && current_output != output.messages) {
           dockable.output.pretty_text_area.update(snapshot, output.results, output.messages)
           current_output = output.messages