suppress document_required GUI element for now: still unused;
authorwenzelm
Mon, 07 Nov 2022 21:53:36 +0100
changeset 76483 49acf5dd58ce
parent 76482 60b963d8fc3c
child 76486 3d281371b213
suppress document_required GUI element for now: still unused;
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