diff -r d5187dd0e5fa -r 7f65a68f8b26 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] =