1.1 --- a/src/Pure/Thy/completion.scala Sun Jun 19 21:38:48 2011 +0200
1.2 +++ b/src/Pure/Thy/completion.scala Sun Jun 19 21:43:41 2011 +0200
1.3 @@ -21,8 +21,8 @@
1.4 {
1.5 override val whiteSpace = "".r
1.6
1.7 - def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
1.8 - def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
1.9 + def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
1.10 + def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
1.11 def word: Parser[String] = "[a-zA-Z0-9_']{2,}".r
1.12
1.13 def read(in: CharSequence): Option[String] =