src/Pure/General/completion.scala
changeset 56039 5ff5208de089
parent 56001 2df1e7bca361
child 56042 d3c35a300433
--- a/src/Pure/General/completion.scala	Mon Mar 10 22:14:53 2014 +0100
+++ b/src/Pure/General/completion.scala	Mon Mar 10 22:22:03 2014 +0100
@@ -211,13 +211,13 @@
     private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
     private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
 
-    private val word_regex = "[a-zA-Z0-9_']+".r
+    private val word_regex = "[a-zA-Z0-9_'.]+".r
     private def word: Parser[String] = word_regex
-    private def word3: Parser[String] = "[a-zA-Z0-9_']{3,}".r
+    private def word3: Parser[String] = "[a-zA-Z0-9_'.]{3,}".r
     private def underscores: Parser[String] = "_*".r
 
     def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
-    def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c)
+    def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == "."
 
     def extend_word(text: CharSequence, offset: Text.Offset): Text.Offset =
     {