# HG changeset patch
# User wenzelm
# Date 1738148029 -3600
# Node ID 82f47e645c0ad7f7248ea5bf2f5d2eb4bfebdce5
# Parent  194de6d02827a5879365ce9f786aef5fe572cd43
more robust: make double sure that buffer.getText() is valid (see also 2e7073976c25);

diff -r 194de6d02827 -r 82f47e645c0a src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Jan 28 21:42:51 2025 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Jan 29 11:53:49 2025 +0100
@@ -166,7 +166,10 @@
     def update(new_info: Option[Text.Info[A]]): Unit = {
       val old_text_info = the_text_info
       val new_text_info =
-        new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
+        for {
+          info <- new_info
+          s <- JEdit_Lib.get_text(text_area.getBuffer, info.range)
+        } yield (s, info)
 
       if (new_text_info != old_text_info) {
         caret_update()