# HG changeset patch
# User wenzelm
# Date 1397560079 -7200
# Node ID 71c5d1f516c0e5b6795f4c0d5a505d74e2b8502b
# Parent  272d173cd3987198a305af3710b48238080a79d4
more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;

diff -r 272d173cd398 -r 71c5d1f516c0 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 12:45:16 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 13:07:59 2014 +0200
@@ -155,13 +155,6 @@
 
       Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
         case Some(syntax) =>
-          val caret = text_area.getCaretPosition
-
-          val line = buffer.getLineOfOffset(caret)
-          val line_start = buffer.getLineStartOffset(line)
-          val line_length = (buffer.getLineEndOffset(line) min buffer.getLength) - line_start
-          val line_text = buffer.getSegment(line_start, line_length)
-
           val context =
             (for {
               rendering <- opt_rendering
@@ -169,8 +162,15 @@
               context <- rendering.language_context(range)
             } yield context) getOrElse syntax.language_context
 
-          syntax.completion.complete(
-            history, decode, explicit, line_start, line_text, caret - line_start, false, context)
+          val caret = text_area.getCaretPosition
+          val line_range = JEdit_Lib.line_range(buffer, text_area.getCaretLine)
+          val line_start = line_range.start
+          for {
+            line_text <- JEdit_Lib.try_get_text(buffer, line_range)
+            result <-
+              syntax.completion.complete(
+                history, decode, explicit, line_start, line_text, caret - line_start, false, context)
+          } yield result
 
         case None => None
       }
diff -r 272d173cd398 -r 71c5d1f516c0 src/Tools/jEdit/src/fold_handling.scala
--- a/src/Tools/jEdit/src/fold_handling.scala	Tue Apr 15 12:45:16 2014 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala	Tue Apr 15 13:07:59 2014 +0200
@@ -38,9 +38,8 @@
 
       if (line <= 0) 0
       else {
-        val start = buffer.getLineStartOffset(line - 1)
-        val end = buffer.getLineEndOffset(line - 1)
-        buffer.getFoldLevel(line - 1) - depth(start - 1) + depth(end - 1)
+        val range = JEdit_Lib.line_range(buffer, line - 1)
+        buffer.getFoldLevel(line - 1) - depth(range.start - 1) + depth(range.stop - 1)
       }
     }
   }
diff -r 272d173cd398 -r 71c5d1f516c0 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 12:45:16 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 13:07:59 2014 +0200
@@ -183,7 +183,7 @@
     Text.Range(0, buffer.getLength)
 
   def line_range(buffer: JEditBuffer, line: Int): Text.Range =
-    Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line))
+    Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength)
 
   def before_caret_range(text_area: TextArea, rendering: Rendering): Option[Text.Range] =
   {