proper Char comparison, despite weakly-typed Scala (cf. 5ff5208de089);
--- 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 =
{