# HG changeset patch # User wenzelm # Date 1498592218 -7200 # Node ID e9fa94f43a15f72bc75c0f5658d6d2749541b624 # Parent b0a30a21f627d4e3c42bf860fe474287880d6d62 tuned signature; diff -r b0a30a21f627 -r e9fa94f43a15 src/Pure/GUI/wrap_panel.scala --- a/src/Pure/GUI/wrap_panel.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Pure/GUI/wrap_panel.scala Tue Jun 27 21:36:58 2017 +0200 @@ -100,18 +100,19 @@ } } } + + def apply(contents: List[Component] = Nil, + alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Center): Wrap_Panel = + new Wrap_Panel(contents, alignment) } - -class Wrap_Panel(alignment: Wrap_Panel.Alignment.Value)(contents0: Component*) +class Wrap_Panel(contents0: List[Component] = Nil, + alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Center) extends Panel with SequentialContainer.Wrapper { override lazy val peer: JPanel = new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin - def this(contents0: Component*) = this(Wrap_Panel.Alignment.Center)(contents0: _*) - def this() = this(Wrap_Panel.Alignment.Center)() - contents ++= contents0 private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout] diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/Graphview/graph_panel.scala --- a/src/Tools/Graphview/graph_panel.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/Graphview/graph_panel.scala Tue Jun 27 21:36:58 2017 +0200 @@ -345,8 +345,10 @@ private val filters = new Button { action = Action("Filters") { mutator_dialog.open } } private val controls = - new Wrap_Panel(Wrap_Panel.Alignment.Right)(show_content, show_arrow_heads, show_dummies, - save_image, zoom, fit_window, update_layout, editor_style) // FIXME colorations, filters + Wrap_Panel( + List(show_content, show_arrow_heads, show_dummies, + save_image, zoom, fit_window, update_layout, editor_style), // FIXME colorations, filters + Wrap_Panel.Alignment.Right) diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/Graphview/tree_panel.scala --- a/src/Tools/Graphview/tree_panel.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/Graphview/tree_panel.scala Tue Jun 27 21:36:58 2017 +0200 @@ -143,7 +143,8 @@ } private val controls = - new Wrap_Panel(Wrap_Panel.Alignment.Right)(selection_label, selection_field, selection_apply) + Wrap_Panel(List(selection_label, selection_field, selection_apply), + Wrap_Panel.Alignment.Right) /* main layout */ diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Tue Jun 27 21:36:58 2017 +0200 @@ -284,11 +284,14 @@ private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } private val controls = - new Wrap_Panel(Wrap_Panel.Alignment.Right)( - break_button, continue_button, step_button, step_over_button, step_out_button, - context_label, Component.wrap(context_field), - expression_label, Component.wrap(expression_field), eval_button, sml_button, - pretty_text_area.search_label, pretty_text_area.search_field, zoom) + Wrap_Panel( + List( + break_button, continue_button, step_button, step_over_button, step_out_button, + context_label, Component.wrap(context_field), + expression_label, Component.wrap(expression_field), eval_button, sml_button, + pretty_text_area.search_label, pretty_text_area.search_field, zoom), + Wrap_Panel.Alignment.Right) + add(controls.peer, BorderLayout.NORTH) diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/info_dockable.scala --- a/src/Tools/jEdit/src/info_dockable.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/info_dockable.scala Tue Jun 27 21:36:58 2017 +0200 @@ -86,8 +86,10 @@ override def componentShown(e: ComponentEvent) { delay_resize.invoke() } }) - private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)( - pretty_text_area.search_label, pretty_text_area.search_field, zoom) + private val controls = + Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom), + Wrap_Panel.Alignment.Right) + add(controls.peer, BorderLayout.NORTH) diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/monitor_dockable.scala --- a/src/Tools/jEdit/src/monitor_dockable.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/monitor_dockable.scala Tue Jun 27 21:36:58 2017 +0200 @@ -95,7 +95,8 @@ } private val controls = - new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats, select_data, reset_data, limit_data) + Wrap_Panel(List(ml_stats, select_data, reset_data, limit_data), + Wrap_Panel.Alignment.Right) /* layout */ diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Tue Jun 27 21:36:58 2017 +0200 @@ -104,8 +104,11 @@ private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } private val controls = - new Wrap_Panel(Wrap_Panel.Alignment.Right)(output_state_button, auto_update_button, - update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom) + Wrap_Panel( + List(output_state_button, auto_update_button, + update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom), + Wrap_Panel.Alignment.Right) + add(controls.peer, BorderLayout.NORTH) diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/protocol_dockable.scala --- a/src/Tools/jEdit/src/protocol_dockable.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/protocol_dockable.scala Tue Jun 27 21:36:58 2017 +0200 @@ -22,7 +22,7 @@ private val ml_stats = new Isabelle.ML_Stats - private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(ml_stats) + private val controls = Wrap_Panel(List(ml_stats), Wrap_Panel.Alignment.Right) /* text area */ diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/query_dockable.scala --- a/src/Tools/jEdit/src/query_dockable.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/query_dockable.scala Tue Jun 27 21:36:58 2017 +0200 @@ -119,10 +119,11 @@ } private val control_panel = - new Wrap_Panel(Wrap_Panel.Alignment.Right)( - query_label, Component.wrap(query), limit, allow_dups, - process_indicator.component, apply_button, - pretty_text_area.search_label, pretty_text_area.search_field) + Wrap_Panel( + List(query_label, Component.wrap(query), limit, allow_dups, + process_indicator.component, apply_button, + pretty_text_area.search_label, pretty_text_area.search_field), + Wrap_Panel.Alignment.Right) def select { control_panel.contents += zoom } @@ -169,9 +170,11 @@ } private val control_panel = - new Wrap_Panel(Wrap_Panel.Alignment.Right)( - query_label, Component.wrap(query), process_indicator.component, apply_button, - pretty_text_area.search_label, pretty_text_area.search_field) + Wrap_Panel( + List( + query_label, Component.wrap(query), process_indicator.component, apply_button, + pretty_text_area.search_label, pretty_text_area.search_field), + Wrap_Panel.Alignment.Right) def select { control_panel.contents += zoom } @@ -255,7 +258,7 @@ } } - private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)() + private val control_panel = Wrap_Panel(Nil, Wrap_Panel.Alignment.Right) def select { diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/simplifier_trace_dockable.scala --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Jun 27 21:36:58 2017 +0200 @@ -153,37 +153,38 @@ /* controls */ - private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)( - new CheckBox("Auto update") { - selected = do_update - reactions += { - case ButtonClicked(_) => - do_update = this.selected - handle_update(do_update) - } - }, - new Button("Update") { - reactions += { - case ButtonClicked(_) => - handle_update(true) - } - }, - new Separator(Orientation.Vertical), - new Button("Show trace") { - reactions += { - case ButtonClicked(_) => - show_trace() - } - }, - new Button("Clear memory") { - reactions += { - case ButtonClicked(_) => - Simplifier_Trace.clear_memory() - } - } - ) + private val controls = + Wrap_Panel(alignment = Wrap_Panel.Alignment.Right, contents = + List( + new CheckBox("Auto update") { + selected = do_update + reactions += { + case ButtonClicked(_) => + do_update = this.selected + handle_update(do_update) + } + }, + new Button("Update") { + reactions += { + case ButtonClicked(_) => + handle_update(true) + } + }, + new Separator(Orientation.Vertical), + new Button("Show trace") { + reactions += { + case ButtonClicked(_) => + show_trace() + } + }, + new Button("Clear memory") { + reactions += { + case ButtonClicked(_) => + Simplifier_Trace.clear_memory() + } + })) - private val answers = new Wrap_Panel(Wrap_Panel.Alignment.Left)() + private val answers = Wrap_Panel(alignment = Wrap_Panel.Alignment.Left) add(controls.peer, BorderLayout.NORTH) add(answers.peer, BorderLayout.SOUTH) diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/simplifier_trace_window.scala --- a/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Jun 27 21:36:58 2017 +0200 @@ -192,10 +192,9 @@ /* controls */ - private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)( - pretty_text_area.search_label, - pretty_text_area.search_field, - zoom) + private val controls = + Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom), + Wrap_Panel.Alignment.Right) peer.add(controls.peer, BorderLayout.NORTH) } diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Jun 27 21:36:58 2017 +0200 @@ -137,9 +137,11 @@ private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } private val controls = - new Wrap_Panel(Wrap_Panel.Alignment.Right)( - provers_label, Component.wrap(provers), isar_proofs, try0, - process_indicator.component, apply_query, cancel_query, locate_query, zoom) + Wrap_Panel( + List(provers_label, Component.wrap(provers), isar_proofs, try0, + process_indicator.component, apply_query, cancel_query, locate_query, zoom), + Wrap_Panel.Alignment.Right) + add(controls.peer, BorderLayout.NORTH) override def focusOnDefaultComponent { provers.requestFocus } diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/state_dockable.scala --- a/src/Tools/jEdit/src/state_dockable.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/state_dockable.scala Tue Jun 27 21:36:58 2017 +0200 @@ -104,8 +104,11 @@ private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } private val controls = - new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update_button, update_button, - locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom) + Wrap_Panel( + List(auto_update_button, update_button, + locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom), + Wrap_Panel.Alignment.Right) + add(controls.peer, BorderLayout.NORTH) diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Tue Jun 27 21:36:58 2017 +0200 @@ -122,7 +122,7 @@ private class Search_Panel extends BorderPanel { val search_field = new TextField(10) - val results_panel = new Wrap_Panel + val results_panel = Wrap_Panel() layout(search_field) = BorderPanel.Position.North layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center @@ -155,12 +155,11 @@ pages ++= Symbol.groups.map({ case (group, symbols) => + val control = group == "control" new TabbedPane.Page(group, - new ScrollPane(new Wrap_Panel { - val control = group == "control" - contents ++= symbols.map(new Symbol_Component(_, control)) - if (control) contents += new Reset_Component - }), null) + new ScrollPane(Wrap_Panel( + symbols.map(new Symbol_Component(_, control)) ::: + (if (control) List(new Reset_Component) else Nil))), null) }) val search_panel = new Search_Panel diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Jun 27 21:36:58 2017 +0200 @@ -85,7 +85,9 @@ private val logic = JEdit_Sessions.logic_selector(PIDE.options.value, true) private val controls = - new Wrap_Panel(Wrap_Panel.Alignment.Right)(purge, continuous_checking, session_phase, logic) + Wrap_Panel(List(purge, continuous_checking, session_phase, logic), + Wrap_Panel.Alignment.Right) + add(controls.peer, BorderLayout.NORTH) diff -r b0a30a21f627 -r e9fa94f43a15 src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Tools/jEdit/src/timing_dockable.scala Tue Jun 27 21:36:58 2017 +0200 @@ -143,7 +143,7 @@ } private val controls = - new Wrap_Panel(Wrap_Panel.Alignment.Right)(threshold_label, threshold_value) + Wrap_Panel(List(threshold_label, threshold_value), Wrap_Panel.Alignment.Right) add(controls.peer, BorderLayout.NORTH)