no word completion within word context;
authorwenzelm
Tue Feb 25 20:46:09 2014 +0100 (2014-02-25)
changeset 557482e1398b484aa
parent 55747 bef19c929ba5
child 55749 75a48dc4383e
no word completion within word context;
src/Pure/General/completion.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Pure/General/completion.scala	Tue Feb 25 20:15:47 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Tue Feb 25 20:46:09 2014 +0100
     1.3 @@ -188,6 +188,12 @@
     1.4  
     1.5    /* word parsers */
     1.6  
     1.7 +  def word_context(text: Option[String]): Boolean =
     1.8 +    text match {
     1.9 +      case None => false
    1.10 +      case Some(s) => Word_Parsers.is_word(s)
    1.11 +    }
    1.12 +
    1.13    private object Word_Parsers extends RegexParsers
    1.14    {
    1.15      override val whiteSpace = "".r
    1.16 @@ -274,6 +280,7 @@
    1.17      explicit: Boolean,
    1.18      text_start: Text.Offset,
    1.19      text: CharSequence,
    1.20 +    word_context: Boolean,
    1.21      context: Completion.Context): Option[Completion.Result] =
    1.22    {
    1.23      val abbrevs_result =
    1.24 @@ -293,18 +300,20 @@
    1.25  
    1.26      val words_result =
    1.27        abbrevs_result orElse {
    1.28 -        Completion.Word_Parsers.read(explicit, text) match {
    1.29 -          case Some(word) =>
    1.30 -            val completions =
    1.31 -              for {
    1.32 -                s <- words_lex.completions(word)
    1.33 -                if (if (keywords(s)) context.is_outer else context.symbols)
    1.34 -                r <- words_map.get_list(s)
    1.35 -              } yield r
    1.36 -            if (completions.isEmpty) None
    1.37 -            else Some(word, completions)
    1.38 -          case None => None
    1.39 -        }
    1.40 +        if (word_context) None
    1.41 +        else
    1.42 +          Completion.Word_Parsers.read(explicit, text) match {
    1.43 +            case Some(word) =>
    1.44 +              val completions =
    1.45 +                for {
    1.46 +                  s <- words_lex.completions(word)
    1.47 +                  if (if (keywords(s)) context.is_outer else context.symbols)
    1.48 +                  r <- words_map.get_list(s)
    1.49 +                } yield r
    1.50 +              if (completions.isEmpty) None
    1.51 +              else Some(word, completions)
    1.52 +            case None => None
    1.53 +          }
    1.54        }
    1.55  
    1.56      words_result match {
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Feb 25 20:15:47 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Feb 25 20:46:09 2014 +0100
     2.3 @@ -137,6 +137,10 @@
     2.4            val start = buffer.getLineStartOffset(line)
     2.5            val text = buffer.getSegment(start, caret - start)
     2.6  
     2.7 +          val word_context =
     2.8 +            Completion.word_context(
     2.9 +              JEdit_Lib.try_get_text(buffer, JEdit_Lib.point_range(buffer, caret)))
    2.10 +
    2.11            val context =
    2.12              (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
    2.13                case Some(rendering) =>
    2.14 @@ -144,7 +148,7 @@
    2.15                case None => None
    2.16              }) getOrElse syntax.completion_context
    2.17  
    2.18 -          syntax.completion.complete(history, decode, explicit, start, text, context)
    2.19 +          syntax.completion.complete(history, decode, explicit, start, text, word_context, context)
    2.20  
    2.21          case None => None
    2.22        }
    2.23 @@ -384,8 +388,13 @@
    2.24            val caret = text_field.getCaret.getDot
    2.25            val text = text_field.getText.substring(0, caret)
    2.26  
    2.27 -          syntax.completion.complete(
    2.28 -              history, decode = true, explicit = false, 0, text, syntax.completion_context) match {
    2.29 +          val word_context =
    2.30 +            Completion.word_context(JEdit_Lib.try_get_text(text_field.getText,
    2.31 +              Text.Range(caret, caret + 1)))  // FIXME proper point range!?
    2.32 +
    2.33 +          val context = syntax.completion_context
    2.34 +
    2.35 +          syntax.completion.complete(history, true, false, 0, text, word_context, context) match {
    2.36              case Some(result) =>
    2.37                val fm = text_field.getFontMetrics(text_field.getFont)
    2.38                val loc =