follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
--- a/src/Tools/jEdit/src/active.scala Sat Aug 09 18:50:39 2014 +0200
+++ b/src/Tools/jEdit/src/active.scala Sun Aug 10 13:06:26 2014 +0200
@@ -48,8 +48,14 @@
GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
}
- case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, _), _) =>
+ case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
+ val link =
+ props match {
+ case Position.Id(id) => PIDE.editor.hyperlink_command_id(snapshot, id)
+ case _ => None
+ }
GUI_Thread.later {
+ link.foreach(_.follow(view))
view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Sat Aug 09 18:50:39 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sun Aug 10 13:06:26 2014 +0200
@@ -246,7 +246,7 @@
def hyperlink_command_id(
snapshot: Document.Snapshot,
id: Document_ID.Generic,
- offset: Symbol.Offset): Option[Hyperlink] =
+ offset: Symbol.Offset = 0): Option[Hyperlink] =
{
snapshot.state.find_command(snapshot.version, id) match {
case Some((node, command)) => hyperlink_command(snapshot, command, offset)