back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
authorwenzelm
Tue Apr 15 19:51:55 2014 +0200 (2014-04-15)
changeset 565930ea7c84110ac
parent 56592 5157f7615e99
child 56594 e3a06699a13f
back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 19:27:50 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 19:51:55 2014 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4          case Some(range) => range.try_restrict(line_range)
     1.5          case None =>
     1.6            if (line_range.contains(text_area.getCaretPosition)) {
     1.7 -            JEdit_Lib.before_caret_range(text_area, rendering) match {
     1.8 +            JEdit_Lib.before_caret_range(text_area, rendering).try_restrict(line_range) match {
     1.9                case Some(range) if !range.is_singularity =>
    1.10                  rendering.semantic_completion(range) match {
    1.11                    case Some(Text.Info(_, Completion.No_Completion)) => None
    1.12 @@ -158,7 +158,7 @@
    1.13            val context =
    1.14              (for {
    1.15                rendering <- opt_rendering
    1.16 -              range <- JEdit_Lib.before_caret_range(text_area, rendering)
    1.17 +              range = JEdit_Lib.before_caret_range(text_area, rendering)
    1.18                context <- rendering.language_context(range)
    1.19              } yield context) getOrElse syntax.language_context
    1.20  
    1.21 @@ -183,13 +183,14 @@
    1.22      {
    1.23        for {
    1.24          spell_checker <- PIDE.spell_checker.get
    1.25 -        caret_range <- JEdit_Lib.before_caret_range(text_area, rendering)
    1.26 -        Text.Info(range, original) <- Spell_Checker.current_word(text_area, rendering, caret_range)
    1.27 -        words = spell_checker.complete(original)
    1.28 +        range = JEdit_Lib.before_caret_range(text_area, rendering)
    1.29 +        word <- Spell_Checker.current_word(text_area, rendering, range)
    1.30 +        words = spell_checker.complete(word.info)
    1.31          if !words.isEmpty
    1.32          descr = "(from dictionary " + quote(spell_checker.toString) + ")"
    1.33 -        items = words.map(w => Completion.Item(range, original, "", List(w, descr), w, 0, false))
    1.34 -      } yield Completion.Result(range, original, false, items)
    1.35 +        items =
    1.36 +          words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
    1.37 +      } yield Completion.Result(word.range, word.info, false, items)
    1.38      }
    1.39  
    1.40  
    1.41 @@ -306,22 +307,20 @@
    1.42              case Some(doc_view) =>
    1.43                val rendering = doc_view.get_rendering()
    1.44                val (no_completion, result) =
    1.45 -                JEdit_Lib.before_caret_range(text_area, rendering) match {
    1.46 -                  case Some(caret_range) =>
    1.47 -                    rendering.semantic_completion(caret_range) match {
    1.48 -                      case Some(Text.Info(_, Completion.No_Completion)) =>
    1.49 -                        (true, None)
    1.50 -                      case Some(Text.Info(range, names: Completion.Names)) =>
    1.51 -                        val result =
    1.52 -                          JEdit_Lib.try_get_text(buffer, range) match {
    1.53 -                            case Some(original) => names.complete(range, history, decode, original)
    1.54 -                            case None => None
    1.55 -                          }
    1.56 -                        (false, result)
    1.57 -                      case None => (false, None)
    1.58 -                    }
    1.59 +              {
    1.60 +                val caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
    1.61 +                rendering.semantic_completion(caret_range) match {
    1.62 +                  case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
    1.63 +                  case Some(Text.Info(range, names: Completion.Names)) =>
    1.64 +                    val result =
    1.65 +                      JEdit_Lib.try_get_text(buffer, range) match {
    1.66 +                        case Some(original) => names.complete(range, history, decode, original)
    1.67 +                        case None => None
    1.68 +                      }
    1.69 +                    (false, result)
    1.70                    case None => (false, None)
    1.71                  }
    1.72 +              }
    1.73                (no_completion, result, Some(rendering))
    1.74              case None => (false, None, None)
    1.75            }
     2.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 19:27:50 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 19:51:55 2014 +0200
     2.3 @@ -190,12 +190,11 @@
     2.4    def caret_range(text_area: TextArea): Text.Range =
     2.5      point_range(text_area.getBuffer, text_area.getCaretPosition)
     2.6  
     2.7 -  def before_caret_range(text_area: TextArea, rendering: Rendering): Option[Text.Range] =
     2.8 +  def before_caret_range(text_area: TextArea, rendering: Rendering): Text.Range =
     2.9    {
    2.10 -    val range = line_range(text_area.getBuffer, text_area.getCaretLine)
    2.11      val snapshot = rendering.snapshot
    2.12      val former_caret = snapshot.revert(text_area.getCaretPosition)
    2.13 -    snapshot.convert(Text.Range(former_caret - 1, former_caret)).try_restrict(range)
    2.14 +    snapshot.convert(Text.Range(former_caret - 1, former_caret))
    2.15    }
    2.16  
    2.17    def visible_range(text_area: TextArea): Option[Text.Range] =