tuned GUI;
authorwenzelm
Wed, 18 Jan 2023 16:22:55 +0100
changeset 77008 60b465c4463c
parent 77007 19a7046f90f9
child 77009 2342b4cc118f
tuned GUI;
src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Jan 18 16:15:41 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Jan 18 16:22:55 2023 +0100
@@ -318,6 +318,7 @@
     Wrap_Panel(List(reset_button, purge_button))
 
   private val theories = new Theories_Status(view, document = true)
+  private val theories_pane = new ScrollPane(theories.gui)
 
   private def refresh_theories(): Unit = {
     val domain = PIDE.editor.document_theories().toSet
@@ -328,7 +329,7 @@
   private val input_page =
     new TabbedPane.Page("Input", new BorderPanel {
       layout(theories_controls) = BorderPanel.Position.North
-      layout(theories.gui) = BorderPanel.Position.Center
+      layout(theories_pane) = BorderPanel.Position.Center
     }, "Selection and status of document theories")
 
   private val output_controls =