# HG changeset patch # User wenzelm # Date 1671624874 -3600 # Node ID c83dfd565283ad84148813e5f2c764a898b90ee8 # Parent c8d5cc19270a3d535054d94e28c184bba4746697 clarified GUI; diff -r c8d5cc19270a -r c83dfd565283 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Wed Dec 21 11:30:24 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Wed Dec 21 13:14:34 2022 +0100 @@ -220,6 +220,12 @@ document_session.reactions += { case SelectionChanged(_) => delay_load.invoke() } + private val load_button = + new GUI.Button("Load") { + tooltip = "Load document theories" + override def clicked(): Unit = PIDE.editor.document_select_all(set = true) + } + private val build_button = new GUI.Button("Build") { tooltip = "Build document" @@ -239,8 +245,8 @@ } private val controls = - Wrap_Panel(List(document_session, process_indicator.component, build_button, - view_button, cancel_button)) + Wrap_Panel(List(document_session, process_indicator.component, load_button, + build_button, view_button, cancel_button)) add(controls.peer, BorderLayout.NORTH) @@ -249,20 +255,19 @@ /* 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" + private val reset_button = + new GUI.Button("Reset") { + tooltip = "Deselect document theories" override def clicked(): Unit = PIDE.editor.document_select_all(set = false) } + private val purge_button = new GUI.Button("Purge") { + tooltip = "Remove theories that are no longer required" + override def clicked(): Unit = PIDE.editor.purge() + } + private val theories_controls = - Wrap_Panel(List(select_all_button, select_none_button)) + Wrap_Panel(List(reset_button, purge_button)) private val theories = new Theories_Status(view, document = true) diff -r c8d5cc19270a -r c83dfd565283 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Wed Dec 21 11:30:24 2022 +0100 +++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Dec 21 13:14:34 2022 +0100 @@ -31,7 +31,7 @@ } private val purge = new GUI.Button("Purge") { - tooltip = "Restrict document model to theories required for open editor buffers" + tooltip = "Remove theories that are no longer required" override def clicked(): Unit = PIDE.editor.purge() }