# HG changeset patch
# User wenzelm
# Date 1482509069 -3600
# Node ID 00aa710ff7f06f35566d4d20ddac306bd3cf8cb6
# Parent  951507563033690d8bdfeab1d6c7fe200cc7ba1e
tuned;

diff -r 951507563033 -r 00aa710ff7f0 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Dec 23 16:20:42 2016 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 23 17:04:29 2016 +0100
@@ -454,6 +454,10 @@
     val load_commands: List[Command]
     def is_loaded: Boolean
 
+    def find_command(id: Document_ID.Generic): Option[(Node, Command)]
+    def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
+      : Option[Line.Node_Position]
+
     def cumulate[A](
       range: Text.Range,
       info: A,
@@ -546,15 +550,6 @@
 
     def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
 
-    def find_command(version: Version, id: Document_ID.Generic): Option[(Node, Command)] =
-      commands.get(id) orElse execs.get(id) match {
-        case None => None
-        case Some(st) =>
-          val command = st.command
-          val node = version.nodes(command.node_name)
-          if (node.commands.contains(command)) Some((node, command)) else None
-      }
-
     def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
     def the_static_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
     def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
@@ -793,6 +788,31 @@
         val is_loaded: Boolean = node_name.is_theory || load_commands.nonEmpty
 
 
+        /* find command */
+
+        def find_command(id: Document_ID.Generic): Option[(Node, Command)] =
+          state.commands.get(id) orElse state.execs.get(id) match {
+            case None => None
+            case Some(st) =>
+              val command = st.command
+              val node = version.nodes(command.node_name)
+              if (node.commands.contains(command)) Some((node, command)) else None
+          }
+
+        def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
+            : Option[Line.Node_Position] =
+          for ((node, command) <- find_command(id))
+          yield {
+            val name = command.node_name.node
+            val sources_iterator =
+              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
+                (if (offset == 0) Iterator.empty
+                 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
+            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
+            Line.Node_Position(name, pos)
+          }
+
+
         /* cumulate markup */
 
         def cumulate[A](
@@ -853,4 +873,3 @@
     }
   }
 }
-
diff -r 951507563033 -r 00aa710ff7f0 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Dec 23 16:20:42 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Dec 23 17:04:29 2016 +0100
@@ -329,7 +329,7 @@
   {
     val buffer = text_area.getBuffer
     if (!snapshot.is_outdated && text != "") {
-      (snapshot.state.find_command(snapshot.version, id), PIDE.document_model(buffer)) match {
+      (snapshot.find_command(id), PIDE.document_model(buffer)) match {
         case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
           node.command_start(command) match {
             case Some(start) =>
diff -r 951507563033 -r 00aa710ff7f0 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 16:20:42 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 17:04:29 2016 +0100
@@ -284,19 +284,7 @@
       : Option[Hyperlink] =
   {
     if (snapshot.is_outdated) None
-    else {
-      snapshot.state.find_command(snapshot.version, id) match {
-        case None => None
-        case Some((node, command)) =>
-          val name = command.node_name.node
-          val sources_iterator =
-            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
-              (if (offset == 0) Iterator.empty
-               else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
-          val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
-          Some(hyperlink_file(focus, Line.Node_Position(name, pos)))
-      }
-    }
+    else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _))
   }
 
   def is_hyperlink_position(snapshot: Document.Snapshot,
@@ -304,7 +292,7 @@
   {
     pos match {
       case Position.Item_Id(id, offset) if offset > 0 =>
-        snapshot.state.find_command(snapshot.version, id) match {
+        snapshot.find_command(id) match {
           case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
             node.command_start(command) match {
               case Some(start) => text_offset == start + command.chunk.decode(offset)