src/Pure/Thy/completion.scala
changeset 44337 7f65a68f8b26
parent 40779 e38e80686ce5
child 44569 5130dfe1b7be
     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] =