# HG changeset patch
# User wenzelm
# Date 1407668786 -7200
# Node ID 51a2f91401756791e50d2f055620602e8447e7e9
# Parent  4faa0b564a5fece92fb45cb8613bf24e4b70bfd5
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);

diff -r 4faa0b564a5f -r 51a2f9140175 src/Tools/jEdit/src/active.scala
--- 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")
                 }
 
diff -r 4faa0b564a5f -r 51a2f9140175 src/Tools/jEdit/src/jedit_editor.scala
--- 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)