clarified layout;
authorwenzelm
Mon, 07 Nov 2022 21:51:14 +0100
changeset 76482 60b963d8fc3c
parent 76481 a9d52d02bd83
child 76483 49acf5dd58ce
clarified layout;
src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Nov 07 21:32:09 2022 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Nov 07 21:51:14 2022 +0100
@@ -10,7 +10,7 @@
 import isabelle._
 
 import scala.swing.{Button, TextArea, Label, ListView, Alignment,
-  ScrollPane, Component, CheckBox, BorderPanel}
+  ScrollPane, Component, CheckBox, BorderPanel, BoxPanel, Orientation}
 import scala.swing.event.{MouseClicked, MouseMoved}
 
 import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
@@ -214,9 +214,12 @@
           BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2))
     }
 
-    layout(theory_required) = BorderPanel.Position.West
+    val required = new BoxPanel(Orientation.Horizontal)
+    required.contents += theory_required
+    required.contents += document_required
+
+    layout(required) = BorderPanel.Position.West
     layout(label) = BorderPanel.Position.Center
-    layout(document_required) = BorderPanel.Position.East
   }
 
   private class Node_Renderer extends ListView.Renderer[Document.Node.Name] {