# 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