# HG changeset patch
# User wenzelm
# Date 1498593416 -7200
# Node ID 2d2082db735adcc36907a2381ec4b5de67383b7a
# Parent  e9fa94f43a15f72bc75c0f5658d6d2749541b624
clarified defaults;

diff -r e9fa94f43a15 -r 2d2082db735a src/Pure/GUI/wrap_panel.scala
--- 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 =
diff -r e9fa94f43a15 -r 2d2082db735a src/Pure/Thy/html.scala
--- 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))),
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/Graphview/graph_panel.scala
--- 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
 
 
 
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/Graphview/tree_panel.scala
--- 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 */
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/VSCode/src/state_panel.scala
--- 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 */
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/debugger_dockable.scala
--- 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)
 
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/info_dockable.scala
--- 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)
 
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/monitor_dockable.scala
--- 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 */
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/output_dockable.scala
--- 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)
 
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/protocol_dockable.scala
--- 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 */
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/query_dockable.scala
--- 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
     {
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- 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)
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/simplifier_trace_window.scala
--- 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)
 }
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/sledgehammer_dockable.scala
--- 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)
 
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/state_dockable.scala
--- 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)
 
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/symbols_dockable.scala
--- 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
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/theories_dockable.scala
--- 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)
 
diff -r e9fa94f43a15 -r 2d2082db735a src/Tools/jEdit/src/timing_dockable.scala
--- 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)