more robust: make double sure that buffer.getText() is valid (see also 2e7073976c25);

--- 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()