# HG changeset patch
# User wenzelm
# Date 1671561820 -3600
# Node ID 37f7b2965e02ada0db0373b58d106874b470ab7f
# Parent  2c8632c746fe019224f7436b1a3e764eb82d6e9e
more GUI operations;

diff -r 2c8632c746fe -r 37f7b2965e02 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Tue Dec 20 19:19:44 2022 +0100
+++ b/src/Pure/PIDE/editor.scala	Tue Dec 20 19:43:40 2022 +0100
@@ -47,6 +47,9 @@
     toggle: Boolean = false
   ): Unit = document_state_change(_.select(names, set = set, toggle = toggle))
 
+  def document_select_all(set: Boolean = false): Unit =
+    document_state_change(st => st.select(st.active_document_theories, set = set))
+
   def document_init(id: AnyRef): Unit = document_state_change(_.register_view(id))
   def document_exit(id: AnyRef): Unit = document_state_change(_.unregister_view(id))
 
diff -r 2c8632c746fe -r 37f7b2965e02 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Dec 20 19:19:44 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Dec 20 19:43:40 2022 +0100
@@ -250,10 +250,26 @@
 
   /* message pane with pages */
 
+  private val select_all_button =
+    new GUI.Button("All") {
+      tooltip = "Select all document theories"
+      override def clicked(): Unit = PIDE.editor.document_select_all(set = true)
+    }
+
+  private val select_none_button =
+    new GUI.Button("None") {
+      tooltip = "Deselect all document theories"
+      override def clicked(): Unit = PIDE.editor.document_select_all(set = false)
+    }
+
+  private val theories_controls =
+    Wrap_Panel(List(select_all_button, select_none_button))
+
   private val theories = new Theories_Status(view, document = true)
 
   private val theories_page =
     new TabbedPane.Page("Theories", new BorderPanel {
+      layout(theories_controls) = BorderPanel.Position.North
       layout(theories.gui) = BorderPanel.Position.Center
     }, "Selection and status of document theories")