src/Pure/Thy/completion.scala
changeset 43462 7f65a68f8b26
parent 40533 e38e80686ce5
child 43695 5130dfe1b7be
--- a/src/Pure/Thy/completion.scala	Sun Jun 19 21:38:48 2011 +0200
+++ b/src/Pure/Thy/completion.scala	Sun Jun 19 21:43:41 2011 +0200
@@ -21,8 +21,8 @@
   {
     override val whiteSpace = "".r
 
-    def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
-    def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
+    def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
+    def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
     def word: Parser[String] = "[a-zA-Z0-9_']{2,}".r
 
     def read(in: CharSequence): Option[String] =