Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned GUI layout;
authorwenzelm
Tue, 06 May 2014 22:55:44 +0200
changeset 56886 87ebb99786ed
parent 56885 3020f6bbd119
child 56887 1ca814da47ae
tuned GUI layout;
src/Tools/jEdit/src/output_dockable.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/query_dockable.scala file | annotate | diff | comparison | revisions 
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue May 06 22:47:55 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue May 06 22:55:44 2014 +0200
@@ -142,7 +142,7 @@
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-      pretty_text_area.search_label, pretty_text_area.search_pattern,
-      auto_update, update, pretty_text_area.detach_button, zoom)
+      auto_update, update, pretty_text_area.detach_button,
+      pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }
--- a/src/Tools/jEdit/src/query_dockable.scala	Tue May 06 22:47:55 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Tue May 06 22:55:44 2014 +0200
@@ -123,9 +123,8 @@
     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_pattern,
-        pretty_text_area.detach_button)
+        process_indicator.component, apply_button, pretty_text_area.detach_button,
+        pretty_text_area.search_label, pretty_text_area.search_pattern)
 
     def select { control_panel.contents += zoom }
 
@@ -172,9 +171,9 @@
 
     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_pattern,
-        pretty_text_area.detach_button)
+        query_label, Component.wrap(query), process_indicator.component,
+        apply_button, pretty_text_area.detach_button,
+        pretty_text_area.search_label, pretty_text_area.search_pattern)
 
     def select { control_panel.contents += zoom }
 
@@ -259,9 +258,8 @@
       set_selector()
       control_panel.contents.clear
       control_panel.contents ++=
-        List(query_label, selector, apply_button,
-          pretty_text_area.search_label, pretty_text_area.search_pattern,
-          pretty_text_area.detach_button, zoom)
+        List(query_label, selector, apply_button, pretty_text_area.detach_button,
+          pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
     }
 
     val page =
isabelle