follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
authorwenzelm
Sun Aug 10 13:06:26 2014 +0200 (2014-08-10)
changeset 5787851a2f9140175
parent 57877 4faa0b564a5f
child 57879 91e188508bc9
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Tools/jEdit/src/active.scala	Sat Aug 09 18:50:39 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/active.scala	Sun Aug 10 13:06:26 2014 +0200
     1.3 @@ -48,8 +48,14 @@
     1.4                    GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
     1.5                  }
     1.6  
     1.7 -              case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, _), _) =>
     1.8 +              case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
     1.9 +                val link =
    1.10 +                  props match {
    1.11 +                    case Position.Id(id) => PIDE.editor.hyperlink_command_id(snapshot, id)
    1.12 +                    case _ => None
    1.13 +                  }
    1.14                  GUI_Thread.later {
    1.15 +                  link.foreach(_.follow(view))
    1.16                    view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
    1.17                  }
    1.18  
     2.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Aug 09 18:50:39 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Aug 10 13:06:26 2014 +0200
     2.3 @@ -246,7 +246,7 @@
     2.4    def hyperlink_command_id(
     2.5      snapshot: Document.Snapshot,
     2.6      id: Document_ID.Generic,
     2.7 -    offset: Symbol.Offset): Option[Hyperlink] =
     2.8 +    offset: Symbol.Offset = 0): Option[Hyperlink] =
     2.9    {
    2.10      snapshot.state.find_command(snapshot.version, id) match {
    2.11        case Some((node, command)) => hyperlink_command(snapshot, command, offset)