# HG changeset patch
# User wenzelm
# Date 1421598758 -3600
# Node ID 39a38657d16b0816f30a835a62cc6f135eb51f02
# Parent  7cab7fdf604898d810a33c5cef5c326e829e1329
tuned;

diff -r 7cab7fdf6048 -r 39a38657d16b src/Tools/Graphview/mutator_dialog.scala
--- a/src/Tools/Graphview/mutator_dialog.scala	Sun Jan 18 17:31:27 2015 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala	Sun Jan 18 17:32:38 2015 +0100
@@ -155,8 +155,8 @@
   contents = new BorderPanel {
     border = new EmptyBorder(5, 5, 5, 5)
 
-    add(new ScrollPane(filter_panel), BorderPanel.Position.Center)
-    add(botPanel, BorderPanel.Position.South)
+    layout(new ScrollPane(filter_panel)) = BorderPanel.Position.Center
+    layout(botPanel) = BorderPanel.Position.South
   }
 
   private class Mutator_Panel(initials: Mutator.Info)
diff -r 7cab7fdf6048 -r 39a38657d16b src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Sun Jan 18 17:31:27 2015 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala	Sun Jan 18 17:32:38 2015 +0100
@@ -126,8 +126,8 @@
 
     val page =
       new TabbedPane.Page("Find Theorems", new BorderPanel {
-        add(control_panel, BorderPanel.Position.North)
-        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+        layout(control_panel) = BorderPanel.Position.North
+        layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
       }, apply_button.tooltip)
   }
 
@@ -174,8 +174,8 @@
 
     val page =
       new TabbedPane.Page("Find Constants", new BorderPanel {
-        add(control_panel, BorderPanel.Position.North)
-        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+        layout(control_panel) = BorderPanel.Position.North
+        layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
       }, apply_button.tooltip)
   }
 
@@ -266,8 +266,8 @@
 
     val page =
       new TabbedPane.Page("Print Context", new BorderPanel {
-        add(control_panel, BorderPanel.Position.North)
-        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+        layout(control_panel) = BorderPanel.Position.North
+        layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
       }, "Print information from context")
   }
 
diff -r 7cab7fdf6048 -r 39a38657d16b src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sun Jan 18 17:31:27 2015 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sun Jan 18 17:32:38 2015 +0100
@@ -64,8 +64,8 @@
     val search_page =
       new TabbedPane.Page("search", new BorderPanel {
         val results_panel = new Wrap_Panel
-        add(search_field, BorderPanel.Position.North)
-        add(new ScrollPane(results_panel), BorderPanel.Position.Center)
+        layout(search_field) = BorderPanel.Position.North
+        layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
   
         val search_space =
           (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList