--- 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]
--- 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)
--- 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 */
--- 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)
--- 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)
--- 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 */
--- 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)
--- 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 */
--- 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
{
--- 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)
--- 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)
}
--- 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 }
--- 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)
--- 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
--- 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)
--- 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)