src/Pure/Thy/thy_syntax.scala
changeset 55118 7df949045dc5
parent 54562 301a721af68b
child 55134 1b67b17cdad5
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Jan 22 17:22:26 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Jan 22 21:33:50 2014 +0100
     1.3 @@ -235,8 +235,10 @@
     1.4          case t :: ts => t :: clean(ts)
     1.5          case Nil => Nil
     1.6        }
     1.7 -    val clean_tokens = clean(tokens.filter(_.is_proper))
     1.8 -    clean_tokens.reverse.find(_.is_name).map(_.content)
     1.9 +    clean(tokens.filter(_.is_proper)) match {
    1.10 +      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
    1.11 +      case _ => None
    1.12 +    }
    1.13    }
    1.14  
    1.15    def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =