# 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); + + + isabelle.jedit.Isabelle.select_structure(textArea); + + 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 */