allow suffix of underscores for words (notably keywords), similar to semantic completion;
authorwenzelm
Sat Mar 08 13:49:01 2014 +0100 (2014-03-08)
changeset 5599613a7d9661ffc
parent 55995 ff7ee9c92d54
child 55997 9dc5ce83202c
allow suffix of underscores for words (notably keywords), similar to semantic completion;
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Sat Mar 08 13:25:56 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Sat Mar 08 13:49:01 2014 +0100
     1.3 @@ -213,7 +213,8 @@
     1.4  
     1.5      private val word_regex = "[a-zA-Z0-9_']+".r
     1.6      private def word: Parser[String] = word_regex
     1.7 -    private def word3: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
     1.8 +    private def word3: Parser[String] = "[a-zA-Z0-9_']{3,}".r
     1.9 +    private def underscores: Parser[String] = "_*".r
    1.10  
    1.11      def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
    1.12      def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c)
    1.13 @@ -237,11 +238,14 @@
    1.14        }
    1.15      }
    1.16  
    1.17 -    def read_word(explicit: Boolean, in: CharSequence): Option[String] =
    1.18 +    def read_word(explicit: Boolean, in: CharSequence): Option[(String, String)] =
    1.19      {
    1.20        val parse_word = if (explicit) word else word3
    1.21        val reverse_in = new Library.Reverse(in)
    1.22 -      parse((reverse_symbol | reverse_symb | escape | parse_word) ^^ (_.reverse), reverse_in) match {
    1.23 +      val parser =
    1.24 +        (reverse_symbol | reverse_symb | escape) ^^ (x => (x.reverse, "")) |
    1.25 +        underscores ~ parse_word ^^ { case x ~ y => (y.reverse, x) }
    1.26 +      parse(parser, reverse_in) match {
    1.27          case Success(result, _) => Some(result)
    1.28          case _ => None
    1.29        }
    1.30 @@ -347,30 +351,32 @@
    1.31          val end =
    1.32            if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
    1.33            else caret
    1.34 -        val opt_word =
    1.35 +        val result =
    1.36            Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match {
    1.37 -            case Some(symbol) => Some(symbol)
    1.38 +            case Some(symbol) => Some((symbol, ""))
    1.39              case None =>
    1.40                val word_context =
    1.41                  end < length && Completion.Word_Parsers.is_word_char(text.charAt(end))
    1.42                if (word_context) None
    1.43                else Completion.Word_Parsers.read_word(explicit, text.subSequence(0, end))
    1.44            }
    1.45 -        opt_word.map(word =>
    1.46 +        result.map(
    1.47            {
    1.48 -            val complete_words = words_lex.completions(word)
    1.49 -            val completions =
    1.50 -              if (complete_words.contains(word)) Nil
    1.51 -              else
    1.52 -                for {
    1.53 -                  complete_word <- complete_words
    1.54 -                  ok =
    1.55 -                    if (is_keyword(complete_word)) language_context.is_outer
    1.56 -                    else language_context.symbols
    1.57 -                  if ok
    1.58 -                  completion <- words_map.get_list(complete_word)
    1.59 -                } yield (complete_word, completion)
    1.60 -            (((word, completions), end))
    1.61 +            case (word, underscores) =>
    1.62 +              val complete_words = words_lex.completions(word)
    1.63 +              val full_word = word + underscores
    1.64 +              val completions =
    1.65 +                if (complete_words.contains(full_word)) Nil
    1.66 +                else
    1.67 +                  for {
    1.68 +                    complete_word <- complete_words
    1.69 +                    ok =
    1.70 +                      if (is_keyword(complete_word)) language_context.is_outer
    1.71 +                      else language_context.symbols
    1.72 +                    if ok
    1.73 +                    completion <- words_map.get_list(complete_word)
    1.74 +                  } yield (complete_word, completion)
    1.75 +              (((full_word, completions), end))
    1.76            })
    1.77        }
    1.78