# HG changeset patch
# User wenzelm
# Date 1730472031 -3600
# Node ID e45d6575f893b7245da9c46547a2ea69936f9f9a
# Parent  74d2e85f245df99e3bfdf30a93c0ddc62f2158c3
more operations;

diff -r 74d2e85f245d -r e45d6575f893 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Oct 29 21:51:21 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Nov 01 15:40:31 2024 +0100
@@ -21,7 +21,7 @@
 import org.gjt.sp.jedit.io.{FileVFS, VFSManager}
 import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator}
 import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter, Selection}
 
 
 object JEdit_Lib {
@@ -179,6 +179,21 @@
   def caret_range(text_area: TextArea): Text.Range =
     point_range(text_area.getBuffer, text_area.getCaretPosition)
 
+  def selection_ranges(text_area: TextArea): List[Text.Range] = {
+    val buffer = text_area.getBuffer
+    text_area.getSelection.toList.flatMap(
+      {
+        case rect: Selection.Rect =>
+          List.from(
+            for {
+              l <- (rect.getStartLine to rect.getEndLine).iterator
+              r = Text.Range(rect.getStart(buffer, l), rect.getEnd(buffer, l))
+              if !r.is_singularity
+            } yield r)
+        case sel: Selection => List(Text.Range(sel.getStart, sel.getEnd))
+      })
+  }
+
   def visible_range(text_area: TextArea): Option[Text.Range] = {
     val buffer = text_area.getBuffer
     val n = text_area.getVisibleLines