# HG changeset patch
# User wenzelm
# Date 1730483747 -3600
# Node ID e85b5f7f9b164beec3daa1382ee56245989b2417
# Parent  228f4b9d1d6706fbe43aaa9739496717d044b5e3
support incremental isabelle.select-structure --- like select-block, but based on selection instead of caret;

diff -r 228f4b9d1d67 -r e85b5f7f9b16 NEWS
--- a/NEWS	Fri Nov 01 18:17:03 2024 +0100
+++ b/NEWS	Fri Nov 01 18:55:47 2024 +0100
@@ -124,7 +124,8 @@
 
 * Action isabelle.select_structure (with keyboard shortcut C+7) extends
 the editor selection by adding the enclosing formal structure, based on
-formal markup by the prover.
+formal markup by the prover. Repeated invocation of this action extends
+the selection incrementally.
 
 * Update to jEdit 5.7.0, the latest release.
 
diff -r 228f4b9d1d67 -r e85b5f7f9b16 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Nov 01 18:17:03 2024 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Nov 01 18:55:47 2024 +0100
@@ -389,7 +389,10 @@
       val sel_ranges = JEdit_Lib.selection_ranges(text_area)
       val caret_range = JEdit_Lib.caret_range(text_area)
       val ranges = if (sel_ranges.isEmpty) List(caret_range) else sel_ranges
-      for (info <- rendering.markup_structure(Rendering.structure_elements, ranges)) {
+      val infos =
+        rendering.markup_structure(Rendering.structure_elements, ranges,
+          filter = markup => !sel_ranges.exists(r => r.contains(markup.range)))
+      for (info <- infos) {
         text_area.addToSelection(new Selection.Range(info.range.start, info.range.stop))
       }
     }