--- a/src/Pure/PIDE/editor.scala Fri Dec 23 15:53:53 2016 +0100
+++ b/src/Pure/PIDE/editor.scala Fri Dec 23 16:20:42 2016 +0100
@@ -28,7 +28,7 @@
def follow(context: Context): Unit
}
def hyperlink_command(
- focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
+ focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
: Option[Hyperlink]
}
--- a/src/Pure/PIDE/query_operation.scala Fri Dec 23 15:53:53 2016 +0100
+++ b/src/Pure/PIDE/query_operation.scala Fri Dec 23 16:20:42 2016 +0100
@@ -208,7 +208,7 @@
for {
command <- state.location
snapshot = editor.node_snapshot(command.node_name)
- link <- editor.hyperlink_command(true, snapshot, command)
+ link <- editor.hyperlink_command(true, snapshot, command.id)
} link.follow(editor_context)
}
--- a/src/Tools/jEdit/src/active.scala Fri Dec 23 15:53:53 2016 +0100
+++ b/src/Tools/jEdit/src/active.scala Fri Dec 23 16:20:42 2016 +0100
@@ -51,7 +51,7 @@
case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
val link =
props match {
- case Position.Id(id) => PIDE.editor.hyperlink_command_id(true, snapshot, id)
+ case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
case _ => None
}
GUI_Thread.later {
--- a/src/Tools/jEdit/src/jedit_editor.scala Fri Dec 23 15:53:53 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Fri Dec 23 16:20:42 2016 +0100
@@ -280,14 +280,14 @@
}
override def hyperlink_command(
- focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
+ focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
: Option[Hyperlink] =
{
if (snapshot.is_outdated) None
else {
- snapshot.state.find_command(snapshot.version, command.id) match {
+ snapshot.state.find_command(snapshot.version, id) match {
case None => None
- case Some((node, _)) =>
+ case Some((node, command)) =>
val name = command.node_name.node
val sources_iterator =
node.commands.iterator.takeWhile(_ != command).map(_.source) ++
@@ -299,16 +299,6 @@
}
}
- def hyperlink_command_id(
- focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
- : Option[Hyperlink] =
- {
- snapshot.state.find_command(snapshot.version, id) match {
- case Some((node, command)) => hyperlink_command(focus, snapshot, command, offset)
- case None => None
- }
- }
-
def is_hyperlink_position(snapshot: Document.Snapshot,
text_offset: Text.Offset, pos: Position.T): Boolean =
{
@@ -332,7 +322,7 @@
case Position.Item_File(name, line, offset) =>
hyperlink_source_file(focus, name, line, offset)
case Position.Item_Id(id, offset) =>
- hyperlink_command_id(focus, snapshot, id, offset)
+ hyperlink_command(focus, snapshot, id, offset)
case _ => None
}
@@ -342,7 +332,7 @@
case Position.Item_Def_File(name, line, offset) =>
hyperlink_source_file(focus, name, line, offset)
case Position.Item_Def_Id(id, offset) =>
- hyperlink_command_id(focus, snapshot, id, offset)
+ hyperlink_command(focus, snapshot, id, offset)
case _ => None
}
}
--- a/src/Tools/jEdit/src/timing_dockable.scala Fri Dec 23 15:53:53 2016 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Fri Dec 23 16:20:42 2016 +0100
@@ -96,7 +96,7 @@
def print: String =
" " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
def follow(snapshot: Document.Snapshot)
- { PIDE.editor.hyperlink_command(true, snapshot, command).foreach(_.follow(view)) }
+ { PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) }
}