equal
deleted
inserted
replaced
121 } |
121 } |
122 |
122 |
123 private val control_panel = |
123 private val control_panel = |
124 new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
124 new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
125 query_label, Component.wrap(query), limit, allow_dups, |
125 query_label, Component.wrap(query), limit, allow_dups, |
126 process_indicator.component, apply_button, |
126 process_indicator.component, apply_button, pretty_text_area.detach_button, |
127 pretty_text_area.search_label, pretty_text_area.search_pattern, |
127 pretty_text_area.search_label, pretty_text_area.search_pattern) |
128 pretty_text_area.detach_button) |
|
129 |
128 |
130 def select { control_panel.contents += zoom } |
129 def select { control_panel.contents += zoom } |
131 |
130 |
132 val page = |
131 val page = |
133 new TabbedPane.Page("Find Theorems", new BorderPanel { |
132 new TabbedPane.Page("Find Theorems", new BorderPanel { |
170 reactions += { case ButtonClicked(_) => apply_query() } |
169 reactions += { case ButtonClicked(_) => apply_query() } |
171 } |
170 } |
172 |
171 |
173 private val control_panel = |
172 private val control_panel = |
174 new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
173 new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
175 query_label, Component.wrap(query), process_indicator.component, apply_button, |
174 query_label, Component.wrap(query), process_indicator.component, |
176 pretty_text_area.search_label, pretty_text_area.search_pattern, |
175 apply_button, pretty_text_area.detach_button, |
177 pretty_text_area.detach_button) |
176 pretty_text_area.search_label, pretty_text_area.search_pattern) |
178 |
177 |
179 def select { control_panel.contents += zoom } |
178 def select { control_panel.contents += zoom } |
180 |
179 |
181 val page = |
180 val page = |
182 new TabbedPane.Page("Find Constants", new BorderPanel { |
181 new TabbedPane.Page("Find Constants", new BorderPanel { |
257 def select |
256 def select |
258 { |
257 { |
259 set_selector() |
258 set_selector() |
260 control_panel.contents.clear |
259 control_panel.contents.clear |
261 control_panel.contents ++= |
260 control_panel.contents ++= |
262 List(query_label, selector, apply_button, |
261 List(query_label, selector, apply_button, pretty_text_area.detach_button, |
263 pretty_text_area.search_label, pretty_text_area.search_pattern, |
262 pretty_text_area.search_label, pretty_text_area.search_pattern, zoom) |
264 pretty_text_area.detach_button, zoom) |
|
265 } |
263 } |
266 |
264 |
267 val page = |
265 val page = |
268 new TabbedPane.Page("Print Context", new BorderPanel { |
266 new TabbedPane.Page("Print Context", new BorderPanel { |
269 add(control_panel, BorderPanel.Position.North) |
267 add(control_panel, BorderPanel.Position.North) |