src/Pure/General/completion.scala
changeset 61613 e4194168a1eb
parent 61600 1ca11ddfcc70
child 61622 8bb7848b3d47
--- 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