--- a/src/Tools/jEdit/src/timing_dockable.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Tue Jun 13 20:16:39 2017 +0200
@@ -88,7 +88,7 @@
{
def print: String =
Time.print_seconds(timing) + "s theory " + quote(name.theory)
- def follow(snapshot: Document.Snapshot) { JEdit_Editor.goto_file(true, view, name.node) }
+ def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(true, view, name.node) }
}
private case class Command_Entry(command: Command, timing: Double) extends Entry
@@ -96,7 +96,7 @@
def print: String =
" " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
def follow(snapshot: Document.Snapshot)
- { JEdit_Editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) }
+ { PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) }
}