completion for control symbols;
authorwenzelm
Sun, 19 Jun 2011 21:43:41 +0200
changeset 43462 7f65a68f8b26
parent 43461 d5187dd0e5fa
child 43463 0a2ffb071fca
completion for control symbols;
src/Pure/Thy/completion.scala
--- 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] =