src/Tools/jEdit/src/completion_popup.scala
changeset 56589 71c5d1f516c0
parent 56587 83777a91f5de
child 56593 0ea7c84110ac
     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        }