equal
deleted
inserted
replaced
142 size = new Dimension(500, 500) |
142 size = new Dimension(500, 500) |
143 contents = new BorderPanel { |
143 contents = new BorderPanel { |
144 layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center |
144 layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center |
145 } |
145 } |
146 |
146 |
147 trace.entries.foreach(System.err.println) |
|
148 |
|
149 private val tree = trace.entries.headOption match { |
147 private val tree = trace.entries.headOption match { |
150 case Some(first) => |
148 case Some(first) => |
151 val tree = new Simplifier_Trace_Window.Root_Tree(first.parent) |
149 val tree = new Simplifier_Trace_Window.Root_Tree(first.parent) |
152 Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree)) |
150 Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree)) |
153 tree |
151 tree |