# HG changeset patch
# User wenzelm
# Date 1667854416 -3600
# Node ID 49acf5dd58cede33b4b5872bb27908e50c28c239
# Parent  60b963d8fc3c7e2c9781b8cfee38fd45f474efe9
suppress document_required GUI element for now: still unused;

diff -r 60b963d8fc3c -r 49acf5dd58ce src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Nov 07 21:51:14 2022 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Nov 07 21:53:36 2022 +0100
@@ -216,7 +216,7 @@
 
     val required = new BoxPanel(Orientation.Horizontal)
     required.contents += theory_required
-    required.contents += document_required
+    // FIXME required.contents += document_required
 
     layout(required) = BorderPanel.Position.West
     layout(label) = BorderPanel.Position.Center