--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Mar 14 21:43:54 2017 +0100
@@ -82,10 +82,10 @@
private def handle_update(follow: Boolean)
{
val (new_snapshot, new_command, new_results, new_id) =
- PIDE.editor.current_node_snapshot(view) match {
+ JEdit_Editor.current_node_snapshot(view) match {
case Some(snapshot) =>
if (follow && !snapshot.is_outdated) {
- PIDE.editor.current_command(view, snapshot) match {
+ JEdit_Editor.current_command(view, snapshot) match {
case Some(cmd) =>
(snapshot, cmd, snapshot.command_results(cmd), cmd.id)
case None =>