# HG changeset patch
# User wenzelm
# Date 1667854274 -3600
# Node ID 60b963d8fc3c7e2c9781b8cfee38fd45f474efe9
# Parent  a9d52d02bd8312ff401eef5167a34c7fabe8fd90
clarified layout;

diff -r a9d52d02bd83 -r 60b963d8fc3c 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] {