more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
authorwenzelm
Tue Apr 15 13:07:59 2014 +0200 (2014-04-15 ago)
changeset 5658971c5d1f516c0
parent 56588 272d173cd398
child 56590 d01d183e84ea
more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/fold_handling.scala
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 12:45:16 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 13:07:59 2014 +0200
     1.3 @@ -155,13 +155,6 @@
     1.4  
     1.5        Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
     1.6          case Some(syntax) =>
     1.7 -          val caret = text_area.getCaretPosition
     1.8 -
     1.9 -          val line = buffer.getLineOfOffset(caret)
    1.10 -          val line_start = buffer.getLineStartOffset(line)
    1.11 -          val line_length = (buffer.getLineEndOffset(line) min buffer.getLength) - line_start
    1.12 -          val line_text = buffer.getSegment(line_start, line_length)
    1.13 -
    1.14            val context =
    1.15              (for {
    1.16                rendering <- opt_rendering
    1.17 @@ -169,8 +162,15 @@
    1.18                context <- rendering.language_context(range)
    1.19              } yield context) getOrElse syntax.language_context
    1.20  
    1.21 -          syntax.completion.complete(
    1.22 -            history, decode, explicit, line_start, line_text, caret - line_start, false, context)
    1.23 +          val caret = text_area.getCaretPosition
    1.24 +          val line_range = JEdit_Lib.line_range(buffer, text_area.getCaretLine)
    1.25 +          val line_start = line_range.start
    1.26 +          for {
    1.27 +            line_text <- JEdit_Lib.try_get_text(buffer, line_range)
    1.28 +            result <-
    1.29 +              syntax.completion.complete(
    1.30 +                history, decode, explicit, line_start, line_text, caret - line_start, false, context)
    1.31 +          } yield result
    1.32  
    1.33          case None => None
    1.34        }
     2.1 --- a/src/Tools/jEdit/src/fold_handling.scala	Tue Apr 15 12:45:16 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/fold_handling.scala	Tue Apr 15 13:07:59 2014 +0200
     2.3 @@ -38,9 +38,8 @@
     2.4  
     2.5        if (line <= 0) 0
     2.6        else {
     2.7 -        val start = buffer.getLineStartOffset(line - 1)
     2.8 -        val end = buffer.getLineEndOffset(line - 1)
     2.9 -        buffer.getFoldLevel(line - 1) - depth(start - 1) + depth(end - 1)
    2.10 +        val range = JEdit_Lib.line_range(buffer, line - 1)
    2.11 +        buffer.getFoldLevel(line - 1) - depth(range.start - 1) + depth(range.stop - 1)
    2.12        }
    2.13      }
    2.14    }
     3.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 12:45:16 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 13:07:59 2014 +0200
     3.3 @@ -183,7 +183,7 @@
     3.4      Text.Range(0, buffer.getLength)
     3.5  
     3.6    def line_range(buffer: JEditBuffer, line: Int): Text.Range =
     3.7 -    Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line))
     3.8 +    Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength)
     3.9  
    3.10    def before_caret_range(text_area: TextArea, rendering: Rendering): Option[Text.Range] =
    3.11    {