equal
deleted
inserted
replaced
74 output.pretty_text_area.update(snapshot, results, info) |
74 output.pretty_text_area.update(snapshot, results, info) |
75 |
75 |
76 private val controls = Wrap_Panel(output.pretty_text_area.search_zoom_components) |
76 private val controls = Wrap_Panel(output.pretty_text_area.search_zoom_components) |
77 add(controls.peer, BorderLayout.NORTH) |
77 add(controls.peer, BorderLayout.NORTH) |
78 |
78 |
79 output.init_gui(dockable, split = true) |
79 output.setup(dockable) |
|
80 set_content(output.split_pane) |
80 |
81 |
81 |
82 |
82 /* main */ |
83 /* main */ |
83 |
84 |
84 private val main = |
85 private val main = |