src/Tools/jEdit/src/simplifier_trace_window.scala
changeset 55556 60ba93d8f9e5
parent 55553 99409ccbe04a
child 55825 694833e3e4a0
     1.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Feb 18 18:43:47 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Feb 18 18:51:03 2014 +0100
     1.3 @@ -146,11 +146,10 @@
     1.4  
     1.5  }
     1.6  
     1.7 -class Simplifier_Trace_Window(view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
     1.8 +
     1.9 +class Simplifier_Trace_Window(
    1.10 +  view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
    1.11  {
    1.12 -
    1.13 -  import Simplifier_Trace_Window._
    1.14 -
    1.15    Swing_Thread.require()
    1.16  
    1.17    val area = new Pretty_Text_Area(view)
    1.18 @@ -162,11 +161,11 @@
    1.19  
    1.20    private val tree = trace.entries.headOption match {
    1.21      case Some(first) =>
    1.22 -      val tree = new Root_Tree(first.parent)
    1.23 -      walk_trace(trace.entries, Map(first.parent -> tree))
    1.24 +      val tree = new Simplifier_Trace_Window.Root_Tree(first.parent)
    1.25 +      Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree))
    1.26        tree
    1.27      case None =>
    1.28 -      new Root_Tree(0)
    1.29 +      new Simplifier_Trace_Window.Root_Tree(0)
    1.30    }
    1.31  
    1.32    do_update(None)