no word completion within word context;
authorwenzelm
Tue, 25 Feb 2014 20:46:09 +0100
changeset 55748 2e1398b484aa
parent 55747 bef19c929ba5
child 55749 75a48dc4383e
no word completion within word context;
src/Pure/General/completion.scala
src/Tools/jEdit/src/completion_popup.scala
--- a/src/Pure/General/completion.scala	Tue Feb 25 20:15:47 2014 +0100
+++ b/src/Pure/General/completion.scala	Tue Feb 25 20:46:09 2014 +0100
@@ -188,6 +188,12 @@
 
   /* word parsers */
 
+  def word_context(text: Option[String]): Boolean =
+    text match {
+      case None => false
+      case Some(s) => Word_Parsers.is_word(s)
+    }
+
   private object Word_Parsers extends RegexParsers
   {
     override val whiteSpace = "".r
@@ -274,6 +280,7 @@
     explicit: Boolean,
     text_start: Text.Offset,
     text: CharSequence,
+    word_context: Boolean,
     context: Completion.Context): Option[Completion.Result] =
   {
     val abbrevs_result =
@@ -293,18 +300,20 @@
 
     val words_result =
       abbrevs_result orElse {
-        Completion.Word_Parsers.read(explicit, text) match {
-          case Some(word) =>
-            val completions =
-              for {
-                s <- words_lex.completions(word)
-                if (if (keywords(s)) context.is_outer else context.symbols)
-                r <- words_map.get_list(s)
-              } yield r
-            if (completions.isEmpty) None
-            else Some(word, completions)
-          case None => None
-        }
+        if (word_context) None
+        else
+          Completion.Word_Parsers.read(explicit, text) match {
+            case Some(word) =>
+              val completions =
+                for {
+                  s <- words_lex.completions(word)
+                  if (if (keywords(s)) context.is_outer else context.symbols)
+                  r <- words_map.get_list(s)
+                } yield r
+              if (completions.isEmpty) None
+              else Some(word, completions)
+            case None => None
+          }
       }
 
     words_result match {
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Feb 25 20:15:47 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Feb 25 20:46:09 2014 +0100
@@ -137,6 +137,10 @@
           val start = buffer.getLineStartOffset(line)
           val text = buffer.getSegment(start, caret - start)
 
+          val word_context =
+            Completion.word_context(
+              JEdit_Lib.try_get_text(buffer, JEdit_Lib.point_range(buffer, caret)))
+
           val context =
             (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
               case Some(rendering) =>
@@ -144,7 +148,7 @@
               case None => None
             }) getOrElse syntax.completion_context
 
-          syntax.completion.complete(history, decode, explicit, start, text, context)
+          syntax.completion.complete(history, decode, explicit, start, text, word_context, context)
 
         case None => None
       }
@@ -384,8 +388,13 @@
           val caret = text_field.getCaret.getDot
           val text = text_field.getText.substring(0, caret)
 
-          syntax.completion.complete(
-              history, decode = true, explicit = false, 0, text, syntax.completion_context) match {
+          val word_context =
+            Completion.word_context(JEdit_Lib.try_get_text(text_field.getText,
+              Text.Range(caret, caret + 1)))  // FIXME proper point range!?
+
+          val context = syntax.completion_context
+
+          syntax.completion.complete(history, true, false, 0, text, word_context, context) match {
             case Some(result) =>
               val fm = text_field.getFontMetrics(text_field.getFont)
               val loc =