--- a/src/Pure/GUI/wrap_panel.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Pure/GUI/wrap_panel.scala Tue Jun 27 21:56:56 2017 +0200
@@ -102,12 +102,12 @@
}
def apply(contents: List[Component] = Nil,
- alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Center): Wrap_Panel =
+ alignment: Alignment.Value = Alignment.Right): Wrap_Panel =
new Wrap_Panel(contents, alignment)
}
class Wrap_Panel(contents0: List[Component] = Nil,
- alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Center)
+ alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Right)
extends Panel with SequentialContainer.Wrapper
{
override lazy val peer: JPanel =
--- a/src/Pure/Thy/html.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Pure/Thy/html.scala Tue Jun 27 21:56:56 2017 +0200
@@ -289,7 +289,7 @@
}
def apply(contents: List[XML.Elem], name: String = "", action: String = "",
- alignment: Alignment.Value = Alignment.center): XML.Elem =
+ alignment: Alignment.Value = Alignment.right): XML.Elem =
{
val body = Library.separate(XML.Text(" "), contents)
GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))),
--- a/src/Tools/Graphview/graph_panel.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/Graphview/graph_panel.scala Tue Jun 27 21:56:56 2017 +0200
@@ -347,8 +347,7 @@
private val controls =
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)
+ save_image, zoom, fit_window, update_layout, editor_style)) // FIXME colorations, filters
--- a/src/Tools/Graphview/tree_panel.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/Graphview/tree_panel.scala Tue Jun 27 21:56:56 2017 +0200
@@ -143,8 +143,7 @@
}
private val controls =
- Wrap_Panel(List(selection_label, selection_field, selection_apply),
- Wrap_Panel.Alignment.Right)
+ Wrap_Panel(List(selection_label, selection_field, selection_apply))
/* main layout */
--- a/src/Tools/VSCode/src/state_panel.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala Tue Jun 27 21:56:56 2017 +0200
@@ -116,9 +116,7 @@
submit = true)
private val controls: XML.Elem =
- HTML.Wrap_Panel(
- contents = List(id_parameter, auto_update_button, update_button, locate_button),
- alignment = HTML.Wrap_Panel.Alignment.right)
+ HTML.Wrap_Panel(List(id_parameter, auto_update_button, update_button, locate_button))
/* main */
--- a/src/Tools/jEdit/src/debugger_dockable.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Tue Jun 27 21:56:56 2017 +0200
@@ -289,8 +289,7 @@
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)
+ pretty_text_area.search_label, pretty_text_area.search_field, zoom))
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/info_dockable.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Tue Jun 27 21:56:56 2017 +0200
@@ -87,8 +87,7 @@
})
private val controls =
- Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom),
- Wrap_Panel.Alignment.Right)
+ Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/monitor_dockable.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Tue Jun 27 21:56:56 2017 +0200
@@ -94,9 +94,7 @@
reactions += { case ValueChanged(_) => input_delay.invoke() }
}
- private val controls =
- Wrap_Panel(List(ml_stats, select_data, reset_data, limit_data),
- Wrap_Panel.Alignment.Right)
+ private val controls = Wrap_Panel(List(ml_stats, select_data, reset_data, limit_data))
/* layout */
--- a/src/Tools/jEdit/src/output_dockable.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Tue Jun 27 21:56:56 2017 +0200
@@ -106,8 +106,7 @@
private val controls =
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)
+ update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/protocol_dockable.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Tue Jun 27 21:56:56 2017 +0200
@@ -22,7 +22,7 @@
private val ml_stats = new Isabelle.ML_Stats
- private val controls = Wrap_Panel(List(ml_stats), Wrap_Panel.Alignment.Right)
+ private val controls = Wrap_Panel(List(ml_stats))
/* text area */
--- a/src/Tools/jEdit/src/query_dockable.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Tue Jun 27 21:56:56 2017 +0200
@@ -122,8 +122,7 @@
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)
+ pretty_text_area.search_label, pretty_text_area.search_field))
def select { control_panel.contents += zoom }
@@ -173,8 +172,7 @@
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)
+ pretty_text_area.search_label, pretty_text_area.search_field))
def select { control_panel.contents += zoom }
@@ -258,7 +256,7 @@
}
}
- private val control_panel = Wrap_Panel(Nil, Wrap_Panel.Alignment.Right)
+ private val control_panel = Wrap_Panel()
def select
{
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Jun 27 21:56:56 2017 +0200
@@ -154,7 +154,7 @@
/* controls */
private val controls =
- Wrap_Panel(alignment = Wrap_Panel.Alignment.Right, contents =
+ Wrap_Panel(
List(
new CheckBox("Auto update") {
selected = do_update
@@ -184,7 +184,7 @@
}
}))
- private val answers = Wrap_Panel(alignment = Wrap_Panel.Alignment.Left)
+ private val answers = Wrap_Panel(Nil, 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 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Jun 27 21:56:56 2017 +0200
@@ -193,8 +193,7 @@
/* controls */
private val controls =
- Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom),
- Wrap_Panel.Alignment.Right)
+ Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
peer.add(controls.peer, BorderLayout.NORTH)
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Jun 27 21:56:56 2017 +0200
@@ -139,8 +139,7 @@
private val controls =
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)
+ process_indicator.component, apply_query, cancel_query, locate_query, zoom))
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/state_dockable.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala Tue Jun 27 21:56:56 2017 +0200
@@ -106,8 +106,7 @@
private val controls =
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)
+ locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/symbols_dockable.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Tue Jun 27 21:56:56 2017 +0200
@@ -47,7 +47,7 @@
tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a)))
}
- private class Abbrevs_Panel extends Wrap_Panel
+ private class Abbrevs_Panel extends Wrap_Panel(Nil, Wrap_Panel.Alignment.Center)
{
private var abbrevs: Thy_Header.Abbrevs = Nil
@@ -122,7 +122,7 @@
private class Search_Panel extends BorderPanel {
val search_field = new TextField(10)
- val results_panel = Wrap_Panel()
+ val results_panel = Wrap_Panel(Nil, Wrap_Panel.Alignment.Center)
layout(search_field) = BorderPanel.Position.North
layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
@@ -159,7 +159,8 @@
new TabbedPane.Page(group,
new ScrollPane(Wrap_Panel(
symbols.map(new Symbol_Component(_, control)) :::
- (if (control) List(new Reset_Component) else Nil))), null)
+ (if (control) List(new Reset_Component) else Nil),
+ Wrap_Panel.Alignment.Center)), null)
})
val search_panel = new Search_Panel
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Jun 27 21:56:56 2017 +0200
@@ -85,8 +85,7 @@
private val logic = JEdit_Sessions.logic_selector(PIDE.options.value, true)
private val controls =
- Wrap_Panel(List(purge, continuous_checking, session_phase, logic),
- Wrap_Panel.Alignment.Right)
+ Wrap_Panel(List(purge, continuous_checking, session_phase, logic))
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/timing_dockable.scala Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Tue Jun 27 21:56:56 2017 +0200
@@ -142,8 +142,8 @@
s match { case Value.Double(x) => x >= 0.0 case _ => false })
}
- private val controls =
- Wrap_Panel(List(threshold_label, threshold_value), Wrap_Panel.Alignment.Right)
+ private val controls = Wrap_Panel(List(threshold_label, threshold_value))
+
add(controls.peer, BorderLayout.NORTH)