equal
deleted
inserted
replaced
123 |
123 |
124 private val control_panel = |
124 private val control_panel = |
125 new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
125 new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
126 query_label, Component.wrap(query), limit, allow_dups, |
126 query_label, Component.wrap(query), limit, allow_dups, |
127 process_indicator.component, apply_button, |
127 process_indicator.component, apply_button, |
128 pretty_text_area.search_label, pretty_text_area.search_pattern) |
128 pretty_text_area.search_label, pretty_text_area.search_field) |
129 |
129 |
130 def select { control_panel.contents += zoom } |
130 def select { control_panel.contents += zoom } |
131 |
131 |
132 val page = |
132 val page = |
133 new TabbedPane.Page("Find Theorems", new BorderPanel { |
133 new TabbedPane.Page("Find Theorems", new BorderPanel { |
171 } |
171 } |
172 |
172 |
173 private val control_panel = |
173 private val control_panel = |
174 new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
174 new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
175 query_label, Component.wrap(query), process_indicator.component, apply_button, |
175 query_label, Component.wrap(query), process_indicator.component, apply_button, |
176 pretty_text_area.search_label, pretty_text_area.search_pattern) |
176 pretty_text_area.search_label, pretty_text_area.search_field) |
177 |
177 |
178 def select { control_panel.contents += zoom } |
178 def select { control_panel.contents += zoom } |
179 |
179 |
180 val page = |
180 val page = |
181 new TabbedPane.Page("Find Constants", new BorderPanel { |
181 new TabbedPane.Page("Find Constants", new BorderPanel { |
266 { |
266 { |
267 set_selector() |
267 set_selector() |
268 control_panel.contents.clear |
268 control_panel.contents.clear |
269 control_panel.contents ++= |
269 control_panel.contents ++= |
270 List(query_label, selector, process_indicator.component, apply_button, |
270 List(query_label, selector, process_indicator.component, apply_button, |
271 pretty_text_area.search_label, pretty_text_area.search_pattern, zoom) |
271 pretty_text_area.search_label, pretty_text_area.search_field, zoom) |
272 } |
272 } |
273 |
273 |
274 val page = |
274 val page = |
275 new TabbedPane.Page("Print Context", new BorderPanel { |
275 new TabbedPane.Page("Print Context", new BorderPanel { |
276 add(control_panel, BorderPanel.Position.North) |
276 add(control_panel, BorderPanel.Position.North) |