clarified before_caret_range: prevent continuation on next line;
authorwenzelm
Tue Apr 15 12:34:16 2014 +0200 (2014-04-15 ago)
changeset 5658783777a91f5de
parent 56586 5ef60881681d
child 56588 272d173cd398
clarified before_caret_range: prevent continuation on next line;
more robust jedit_text_areas in unclear situations of object initialization;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 11:26:17 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 12:34:16 2014 +0200
     1.3 @@ -126,9 +126,8 @@
     1.4        active_range match {
     1.5          case Some(range) => range.try_restrict(line_range)
     1.6          case None =>
     1.7 -          val buffer = text_area.getBuffer
     1.8            if (line_range.contains(text_area.getCaretPosition)) {
     1.9 -            JEdit_Lib.before_caret_range(text_area, rendering).try_restrict(line_range) match {
    1.10 +            JEdit_Lib.before_caret_range(text_area, rendering) match {
    1.11                case Some(range) if !range.is_singularity =>
    1.12                  rendering.semantic_completion(range) match {
    1.13                    case Some(Text.Info(_, Completion.No_Completion)) => None
    1.14 @@ -164,11 +163,11 @@
    1.15            val line_text = buffer.getSegment(line_start, line_length)
    1.16  
    1.17            val context =
    1.18 -            (opt_rendering match {
    1.19 -              case Some(rendering) =>
    1.20 -                rendering.language_context(JEdit_Lib.before_caret_range(text_area, rendering))
    1.21 -              case None => None
    1.22 -            }) getOrElse syntax.language_context
    1.23 +            (for {
    1.24 +              rendering <- opt_rendering
    1.25 +              range <- JEdit_Lib.before_caret_range(text_area, rendering)
    1.26 +              context <- rendering.language_context(range)
    1.27 +            } yield context) getOrElse syntax.language_context
    1.28  
    1.29            syntax.completion.complete(
    1.30              history, decode, explicit, line_start, line_text, caret - line_start, false, context)
    1.31 @@ -181,23 +180,17 @@
    1.32      /* spell-checker completion */
    1.33  
    1.34      def spell_checker_completion(rendering: Rendering): Option[Completion.Result] =
    1.35 -      PIDE.spell_checker.get match {
    1.36 -        case Some(spell_checker) =>
    1.37 -          val caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
    1.38 -          Spell_Checker.current_word(text_area, rendering, caret_range) match {
    1.39 -            case Some(Text.Info(range, original)) =>
    1.40 -              val words = spell_checker.complete(original)
    1.41 -              if (words.isEmpty) None
    1.42 -              else {
    1.43 -                val descr = "(from dictionary " + quote(spell_checker.toString) + ")"
    1.44 -                val items = words.map(word =>
    1.45 -                  Completion.Item(range, original, "", List(word, descr), word, 0, false))
    1.46 -                Some(Completion.Result(range, original, false, items))
    1.47 -              }
    1.48 -            case None => None
    1.49 -          }
    1.50 -        case None => None
    1.51 -      }
    1.52 +    {
    1.53 +      for {
    1.54 +        spell_checker <- PIDE.spell_checker.get
    1.55 +        caret_range <- JEdit_Lib.before_caret_range(text_area, rendering)
    1.56 +        Text.Info(range, original) <- Spell_Checker.current_word(text_area, rendering, caret_range)
    1.57 +        words = spell_checker.complete(original)
    1.58 +        if !words.isEmpty
    1.59 +        descr = "(from dictionary " + quote(spell_checker.toString) + ")"
    1.60 +        items = words.map(w => Completion.Item(range, original, "", List(w, descr), w, 0, false))
    1.61 +      } yield Completion.Result(range, original, false, items)
    1.62 +    }
    1.63  
    1.64  
    1.65      /* completion action: text area */
    1.66 @@ -313,23 +306,24 @@
    1.67              case Some(doc_view) =>
    1.68                val rendering = doc_view.get_rendering()
    1.69                val (no_completion, result) =
    1.70 -                rendering.semantic_completion(JEdit_Lib.before_caret_range(text_area, rendering))
    1.71 -                match {
    1.72 -                  case Some(Text.Info(_, Completion.No_Completion)) =>
    1.73 -                    (true, None)
    1.74 -                  case Some(Text.Info(range, names: Completion.Names)) =>
    1.75 -                    val result =
    1.76 -                      JEdit_Lib.try_get_text(buffer, range) match {
    1.77 -                        case Some(original) => names.complete(range, history, decode, original)
    1.78 -                        case None => None
    1.79 -                      }
    1.80 -                    (false, result)
    1.81 -                  case None =>
    1.82 -                    (false, None)
    1.83 +                JEdit_Lib.before_caret_range(text_area, rendering) match {
    1.84 +                  case Some(caret_range) =>
    1.85 +                    rendering.semantic_completion(caret_range) match {
    1.86 +                      case Some(Text.Info(_, Completion.No_Completion)) =>
    1.87 +                        (true, None)
    1.88 +                      case Some(Text.Info(range, names: Completion.Names)) =>
    1.89 +                        val result =
    1.90 +                          JEdit_Lib.try_get_text(buffer, range) match {
    1.91 +                            case Some(original) => names.complete(range, history, decode, original)
    1.92 +                            case None => None
    1.93 +                          }
    1.94 +                        (false, result)
    1.95 +                      case None => (false, None)
    1.96 +                    }
    1.97 +                  case None => (false, None)
    1.98                  }
    1.99                (no_completion, result, Some(rendering))
   1.100 -            case None =>
   1.101 -              (false, None, None)
   1.102 +            case None => (false, None, None)
   1.103            }
   1.104          }
   1.105          if (no_completion) false
   1.106 @@ -339,8 +333,8 @@
   1.107              val result0 =
   1.108                if (word_only) None
   1.109                else
   1.110 -                Completion.Result.merge(history,
   1.111 -                  semantic_completion, syntax_completion(history, explicit, opt_rendering))
   1.112 +                Completion.Result.merge(history, semantic_completion,
   1.113 +                  syntax_completion(history, explicit, opt_rendering))
   1.114              opt_rendering match {
   1.115                case None => result0
   1.116                case Some(rendering) =>
     2.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Apr 15 11:26:17 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Apr 15 12:34:16 2014 +0200
     2.3 @@ -299,7 +299,7 @@
     2.4        spell_checker <- PIDE.spell_checker.get
     2.5        doc_view <- PIDE.document_view(text_area)
     2.6        rendering = doc_view.get_rendering()
     2.7 -      range = JEdit_Lib.before_caret_range(text_area, rendering)
     2.8 +      range <- JEdit_Lib.before_caret_range(text_area, rendering)
     2.9        Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
    2.10      } {
    2.11        spell_checker.update(word, include, permanent)
     3.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 11:26:17 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 12:34:16 2014 +0200
     3.3 @@ -126,7 +126,8 @@
     3.4    def jedit_views(): Iterator[View] = jEdit.getViews().iterator
     3.5  
     3.6    def jedit_text_areas(view: View): Iterator[JEditTextArea] =
     3.7 -    view.getEditPanes().iterator.map(_.getTextArea)
     3.8 +    if (view == null) Iterator.empty
     3.9 +    else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null)
    3.10  
    3.11    def jedit_text_areas(): Iterator[JEditTextArea] =
    3.12      jedit_views().flatMap(jedit_text_areas(_))
    3.13 @@ -176,21 +177,22 @@
    3.14      }
    3.15  
    3.16  
    3.17 -  /* caret */
    3.18 -
    3.19 -  def before_caret_range(text_area: TextArea, rendering: Rendering): Text.Range =
    3.20 -  {
    3.21 -    val snapshot = rendering.snapshot
    3.22 -    val former_caret = snapshot.revert(text_area.getCaretPosition)
    3.23 -    snapshot.convert(Text.Range(former_caret - 1, former_caret))
    3.24 -  }
    3.25 -
    3.26 -
    3.27    /* text ranges */
    3.28  
    3.29    def buffer_range(buffer: JEditBuffer): Text.Range =
    3.30      Text.Range(0, buffer.getLength)
    3.31  
    3.32 +  def line_range(buffer: JEditBuffer, line: Int): Text.Range =
    3.33 +    Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line))
    3.34 +
    3.35 +  def before_caret_range(text_area: TextArea, rendering: Rendering): Option[Text.Range] =
    3.36 +  {
    3.37 +    val range = line_range(text_area.getBuffer, text_area.getCaretLine)
    3.38 +    val snapshot = rendering.snapshot
    3.39 +    val former_caret = snapshot.revert(text_area.getCaretPosition)
    3.40 +    snapshot.convert(Text.Range(former_caret - 1, former_caret)).try_restrict(range)
    3.41 +  }
    3.42 +
    3.43    def visible_range(text_area: TextArea): Option[Text.Range] =
    3.44    {
    3.45      val buffer = text_area.getBuffer