back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
authorwenzelm
Tue, 15 Apr 2014 19:51:55 +0200
changeset 56593 0ea7c84110ac
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
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 19:27:50 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 19:51:55 2014 +0200
@@ -127,7 +127,7 @@
         case Some(range) => range.try_restrict(line_range)
         case None =>
           if (line_range.contains(text_area.getCaretPosition)) {
-            JEdit_Lib.before_caret_range(text_area, rendering) match {
+            JEdit_Lib.before_caret_range(text_area, rendering).try_restrict(line_range) match {
               case Some(range) if !range.is_singularity =>
                 rendering.semantic_completion(range) match {
                   case Some(Text.Info(_, Completion.No_Completion)) => None
@@ -158,7 +158,7 @@
           val context =
             (for {
               rendering <- opt_rendering
-              range <- JEdit_Lib.before_caret_range(text_area, rendering)
+              range = JEdit_Lib.before_caret_range(text_area, rendering)
               context <- rendering.language_context(range)
             } yield context) getOrElse syntax.language_context
 
@@ -183,13 +183,14 @@
     {
       for {
         spell_checker <- PIDE.spell_checker.get
-        caret_range <- JEdit_Lib.before_caret_range(text_area, rendering)
-        Text.Info(range, original) <- Spell_Checker.current_word(text_area, rendering, caret_range)
-        words = spell_checker.complete(original)
+        range = JEdit_Lib.before_caret_range(text_area, rendering)
+        word <- Spell_Checker.current_word(text_area, rendering, range)
+        words = spell_checker.complete(word.info)
         if !words.isEmpty
         descr = "(from dictionary " + quote(spell_checker.toString) + ")"
-        items = words.map(w => Completion.Item(range, original, "", List(w, descr), w, 0, false))
-      } yield Completion.Result(range, original, false, items)
+        items =
+          words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
+      } yield Completion.Result(word.range, word.info, false, items)
     }
 
 
@@ -306,22 +307,20 @@
             case Some(doc_view) =>
               val rendering = doc_view.get_rendering()
               val (no_completion, result) =
-                JEdit_Lib.before_caret_range(text_area, rendering) match {
-                  case Some(caret_range) =>
-                    rendering.semantic_completion(caret_range) match {
-                      case Some(Text.Info(_, Completion.No_Completion)) =>
-                        (true, None)
-                      case Some(Text.Info(range, names: Completion.Names)) =>
-                        val result =
-                          JEdit_Lib.try_get_text(buffer, range) match {
-                            case Some(original) => names.complete(range, history, decode, original)
-                            case None => None
-                          }
-                        (false, result)
-                      case None => (false, None)
-                    }
+              {
+                val caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
+                rendering.semantic_completion(caret_range) match {
+                  case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
+                  case Some(Text.Info(range, names: Completion.Names)) =>
+                    val result =
+                      JEdit_Lib.try_get_text(buffer, range) match {
+                        case Some(original) => names.complete(range, history, decode, original)
+                        case None => None
+                      }
+                    (false, result)
                   case None => (false, None)
                 }
+              }
               (no_completion, result, Some(rendering))
             case None => (false, None, None)
           }
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 19:27:50 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 15 19:51:55 2014 +0200
@@ -190,12 +190,11 @@
   def caret_range(text_area: TextArea): Text.Range =
     point_range(text_area.getBuffer, text_area.getCaretPosition)
 
-  def before_caret_range(text_area: TextArea, rendering: Rendering): Option[Text.Range] =
+  def before_caret_range(text_area: TextArea, rendering: Rendering): Text.Range =
   {
-    val range = line_range(text_area.getBuffer, text_area.getCaretLine)
     val snapshot = rendering.snapshot
     val former_caret = snapshot.revert(text_area.getCaretPosition)
-    snapshot.convert(Text.Range(former_caret - 1, former_caret)).try_restrict(range)
+    snapshot.convert(Text.Range(former_caret - 1, former_caret))
   }
 
   def visible_range(text_area: TextArea): Option[Text.Range] =