diff -r 1403a22e5538 -r d3c35a300433 src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Mon Mar 10 22:39:37 2014 +0100 +++ b/src/Pure/General/completion.scala Mon Mar 10 22:40:48 2014 +0100 @@ -217,7 +217,7 @@ 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) || c == "." + def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.' def extend_word(text: CharSequence, offset: Text.Offset): Text.Offset = {