# HG changeset patch
# User wenzelm
# Date 1730485252 -3600
# Node ID af9be588f62fc38a346dec75b2d3905bc7af9c3d
# Parent  42b9bd119d2b769577edab7b2891f8b8cd8822f7
clarified treatment of caret_range: better support for multiple (unrelated) selections;

diff -r 42b9bd119d2b -r af9be588f62f src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Nov 01 19:11:40 2024 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Nov 01 19:20:52 2024 +0100
@@ -388,9 +388,8 @@
     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
       val infos =
-        rendering.markup_structure(Rendering.structure_elements, ranges,
+        rendering.markup_structure(Rendering.structure_elements, List(caret_range),
           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))