# HG changeset patch
# User wenzelm
# Date 1730476390 -3600
# Node ID 42ff2b915b1daa54d41c51c2b5f0aa2db43f2f35
# Parent  e45d6575f893b7245da9c46547a2ea69936f9f9a
support Isabelle/jEdit action isabelle.select_structure;
update component jedit-20241101;

diff -r e45d6575f893 -r 42ff2b915b1d Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri Nov 01 15:40:31 2024 +0100
+++ b/Admin/components/components.sha1	Fri Nov 01 16:53:10 2024 +0100
@@ -242,6 +242,7 @@
 f4f3fcbd54488297a5d2fcd23a2595912d5ba80b jedit-20211103.tar.gz
 7fc9df033ec6b49dc1dad85eb240ab4f80653aa3 jedit-20231120.tar.gz
 fbfd1d8a117a5bd844f230903d561cb88d3e5189 jedit-20240425.tar.gz
+5117b7d0283adf31cf2bde17a9912eb775a0822f jedit-20241101.tar.gz
 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
 a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
diff -r e45d6575f893 -r 42ff2b915b1d Admin/components/main
--- a/Admin/components/main	Fri Nov 01 15:40:31 2024 +0100
+++ b/Admin/components/main	Fri Nov 01 16:53:10 2024 +0100
@@ -14,7 +14,7 @@
 isabelle_setup-20240327
 javamail-20240109
 jdk-21.0.3
-jedit-20240425
+jedit-20241101
 jfreechart-1.5.3
 jortho-1.0-2
 jsoup-1.17.2
diff -r e45d6575f893 -r 42ff2b915b1d NEWS
--- a/NEWS	Fri Nov 01 15:40:31 2024 +0100
+++ b/NEWS	Fri Nov 01 16:53:10 2024 +0100
@@ -120,6 +120,13 @@
   unbundle no datatype_record_syntax
 
 
+*** Isabelle/jEdit Prover IDE ***
+
+* 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.
+
+
 *** Isabelle/VSCode Prover IDE ***
 
 * General improvements: Persistent decorations for PIDE markup, correct
diff -r e45d6575f893 -r 42ff2b915b1d src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Fri Nov 01 15:40:31 2024 +0100
+++ b/src/Pure/Admin/component_jedit.scala	Fri Nov 01 16:53:10 2024 +0100
@@ -316,6 +316,8 @@
 isabelle.reset-words.label=Reset non-permanent words
 isabelle.select-entity.label=Select all occurences of formal entity at caret
 isabelle.select-entity.shortcut=CS+ENTER
+isabelle.select-structure.label=Select structure around selection or caret
+isabelle.select-structure.shortcut=C+7
 isabelle.set-continuous-checking.label=Set continuous checking
 isabelle.set-node-required.label=Set node required
 isabelle.toggle-breakpoint.label=Toggle Breakpoint
diff -r e45d6575f893 -r 42ff2b915b1d src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Fri Nov 01 15:40:31 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala	Fri Nov 01 16:53:10 2024 +0100
@@ -222,6 +222,11 @@
 
   val text_color_elements = Markup.Elements(text_color.keySet)
 
+  val structure_elements =
+    Markup.Elements(Markup.NOTATION, Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,
+      Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
+      Markup.COMMAND_SPAN)
+
   val tooltip_elements =
     Markup.Elements(Markup.LANGUAGE, Markup.NOTATION, Markup.EXPRESSION, Markup.TIMING,
       Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
@@ -572,6 +577,26 @@
   }
 
 
+  /* markup structure */
+
+  def markup_structure(
+    elements: Markup.Elements,
+    ranges: List[Text.Range],
+    filter: Text.Markup => Boolean = _ => true
+  ): List[Text.Markup] = {
+    def cumulate(range: Text.Range): List[Text.Info[Option[Text.Markup]]] =
+      snapshot.cumulate[Option[Text.Markup]](range, None, elements, _ =>
+        {
+          case (old, markup) =>
+            Some(if (old.isEmpty || filter(markup)) Some(markup) else old)
+        })
+
+    Library.distinct(
+      for (range <- ranges; case Text.Info(_, Some(m)) <- cumulate(range))
+        yield m)
+  }
+
+
   /* tooltips */
 
   def timing_threshold: Double = 0.0
diff -r e45d6575f893 -r 42ff2b915b1d src/Tools/jEdit/jedit_main/actions.xml
--- a/src/Tools/jEdit/jedit_main/actions.xml	Fri Nov 01 15:40:31 2024 +0100
+++ b/src/Tools/jEdit/jedit_main/actions.xml	Fri Nov 01 16:53:10 2024 +0100
@@ -82,6 +82,11 @@
 	    isabelle.jedit.Isabelle.select_entity(textArea);
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.select-structure">
+	  <CODE>
+	    isabelle.jedit.Isabelle.select_structure(textArea);
+	  </CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.complete">
 	  <CODE>
 	    isabelle.jedit.Isabelle.complete(view, false);
diff -r e45d6575f893 -r 42ff2b915b1d src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Nov 01 15:40:31 2024 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Nov 01 16:53:10 2024 +0100
@@ -360,7 +360,7 @@
   }
 
 
-  /* formal entities */
+  /* formal entities and structure */
 
   def goto_entity(view: View): Unit = {
     val text_area = view.getTextArea
@@ -384,6 +384,17 @@
     }
   }
 
+  def select_structure(text_area: JEditTextArea): Unit = {
+    for (rendering <- Document_View.get_rendering(text_area)) {
+      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)) {
+        text_area.addToSelection(new Selection.Range(info.range.start, info.range.stop))
+      }
+    }
+  }
+
 
   /* completion */