include long identifiers in the reckoning of words (e.g. "integer.lifting" vs. 'lifting_update');
authorwenzelm
Mon Mar 10 22:22:03 2014 +0100 (2014-03-10)
changeset 560395ff5208de089
parent 56038 0e2dec666152
child 56040 98d466e6de8a
include long identifiers in the reckoning of words (e.g. "integer.lifting" vs. 'lifting_update');
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Mon Mar 10 22:14:53 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Mon Mar 10 22:22:03 2014 +0100
     1.3 @@ -211,13 +211,13 @@
     1.4      private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
     1.5      private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
     1.6  
     1.7 -    private val word_regex = "[a-zA-Z0-9_']+".r
     1.8 +    private val word_regex = "[a-zA-Z0-9_'.]+".r
     1.9      private def word: Parser[String] = word_regex
    1.10 -    private def word3: Parser[String] = "[a-zA-Z0-9_']{3,}".r
    1.11 +    private def word3: Parser[String] = "[a-zA-Z0-9_'.]{3,}".r
    1.12      private def underscores: Parser[String] = "_*".r
    1.13  
    1.14      def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
    1.15 -    def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c)
    1.16 +    def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == "."
    1.17  
    1.18      def extend_word(text: CharSequence, offset: Text.Offset): Text.Offset =
    1.19      {