src/Pure/Thy/thy_syntax.scala
changeset 38239 89a4d1028fb3
parent 36956 21be4832c362
child 38373 e8197eea3cd0
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Sun Aug 08 20:03:31 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Aug 08 22:33:41 2010 +0200
     1.3 @@ -7,30 +7,29 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import scala.collection.mutable
     1.8 +
     1.9 +
    1.10  object Thy_Syntax
    1.11  {
    1.12 -  private val parser = new Parse.Parser
    1.13 -  {
    1.14 -    override def filter_proper = false
    1.15 -
    1.16 -    val command_span: Parser[Span] =
    1.17 -    {
    1.18 -      val whitespace = token("white space", _.is_ignored)
    1.19 -      val command = token("command keyword", _.is_command)
    1.20 -      val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof
    1.21 -      command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body)
    1.22 -    }
    1.23 -  }
    1.24 -
    1.25    type Span = List[Token]
    1.26  
    1.27    def parse_spans(toks: List[Token]): List[Span] =
    1.28    {
    1.29 -    import parser._
    1.30 +    val result = new mutable.ListBuffer[Span]
    1.31 +    val span = new mutable.ListBuffer[Token]
    1.32 +    val whitespace = new mutable.ListBuffer[Token]
    1.33  
    1.34 -    parse(rep(command_span), Token.reader(toks)) match {
    1.35 -      case Success(spans, rest) if rest.atEnd => spans
    1.36 -      case bad => error(bad.toString)
    1.37 +    def flush(buffer: mutable.ListBuffer[Token])
    1.38 +    {
    1.39 +      if (!buffer.isEmpty) { result += buffer.toList; buffer.clear }
    1.40      }
    1.41 +    for (tok <- toks) {
    1.42 +      if (tok.is_command) { flush(span); flush(whitespace); span += tok }
    1.43 +      else if (tok.is_ignored) whitespace += tok
    1.44 +      else { span ++= whitespace; whitespace.clear; span += tok }
    1.45 +    }
    1.46 +    flush(span); flush(whitespace)
    1.47 +    result.toList
    1.48    }
    1.49  }