--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Feb 18 18:43:47 2014 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Feb 18 18:51:03 2014 +0100
@@ -10,7 +10,6 @@
import isabelle._
import scala.actors.Actor._
-
import scala.swing.{Button, CheckBox, Orientation, Separator}
import scala.swing.event.ButtonClicked
@@ -19,6 +18,7 @@
import org.gjt.sp.jedit.View
+
class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
{
Swing_Thread.require()
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 18 18:43:47 2014 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Feb 18 18:51:03 2014 +0100
@@ -146,11 +146,10 @@
}
-class Simplifier_Trace_Window(view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
+
+class Simplifier_Trace_Window(
+ view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
{
-
- import Simplifier_Trace_Window._
-
Swing_Thread.require()
val area = new Pretty_Text_Area(view)
@@ -162,11 +161,11 @@
private val tree = trace.entries.headOption match {
case Some(first) =>
- val tree = new Root_Tree(first.parent)
- walk_trace(trace.entries, Map(first.parent -> tree))
+ val tree = new Simplifier_Trace_Window.Root_Tree(first.parent)
+ Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree))
tree
case None =>
- new Root_Tree(0)
+ new Simplifier_Trace_Window.Root_Tree(0)
}
do_update(None)