# 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