# HG changeset patch
# User wenzelm
# Date 1447167839 -3600
# Node ID e4194168a1eb3d8106c164d7e16f8fa1d0a07786
# Parent  a99125aa964f4819b24933d2a8656cfde8f3d465
allow open symboloid;

diff -r a99125aa964f -r e4194168a1eb src/Pure/General/completion.scala
--- 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