--- 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))
--- 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")