--- a/src/Pure/General/completion.scala Mon Nov 09 22:16:04 2015 +0100
+++ b/src/Pure/General/completion.scala Tue Nov 10 16:03:59 2015 +0100
@@ -246,7 +246,7 @@
{
override val whiteSpace = "".r
- private val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>)""".r
+ private val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>?)""".r
def is_symboloid(s: CharSequence): Boolean = symboloid_regex.pattern.matcher(s).matches
private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r