# HG changeset patch
# User wenzelm
# Date 1762095205 -3600
# Node ID d9059089359b0f1586dbce0699e96fa4f725e7e0
# Parent  1cd0ab0ccb9dda38aeccd507b6973b9b5541e2b5
tuned signature: more operations;

diff -r 1cd0ab0ccb9d -r d9059089359b src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Sun Nov 02 15:53:04 2025 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Sun Nov 02 15:53:25 2025 +0100
@@ -191,16 +191,20 @@
     }
   }
 
-  def locate_query(): Unit = {
-    editor.require_dispatcher {}
+  def query_command(): Option[(Document.Snapshot, Command)] =
+    editor.require_dispatcher {
+      val state = current_state.value
+      for {
+        command <- state.location
+        snapshot = editor.node_snapshot(command.node_name) if !snapshot.is_outdated
+      } yield (snapshot, command)
+    }
 
-    val state = current_state.value
+  def locate_query(): Unit =
     for {
-      command <- state.location
-      snapshot = editor.node_snapshot(command.node_name)
+      (snapshot, command) <- query_command()
       link <- editor.hyperlink_command(true, snapshot, command.id)
     } link.follow(editor_context)
-  }
 
 
   /* main */