src/Pure/Thy/thy_syntax.scala
author wenzelm
Sat May 15 22:15:57 2010 +0200 (2010-05-15)
changeset 36948 d2cdad45fd14
parent 34311 f0a6f02ad705
child 36956 21be4832c362
permissions -rw-r--r--
renamed Outer_Parse to Parse (in Scala);
     1 /*  Title:      Pure/Thy/thy_syntax.scala
     2     Author:     Makarius
     3 
     4 Superficial theory syntax: command spans.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Thy_Syntax
    11 {
    12   private val parser = new Parse.Parser
    13   {
    14     override def filter_proper = false
    15 
    16     val command_span: Parser[Span] =
    17     {
    18       val whitespace = token("white space", _.is_ignored)
    19       val command = token("command keyword", _.is_command)
    20       val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof
    21       command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body)
    22     }
    23   }
    24 
    25   type Span = List[Outer_Lex.Token]
    26 
    27   def parse_spans(toks: List[Outer_Lex.Token]): List[Span] =
    28   {
    29     import parser._
    30 
    31     parse(rep(command_span), Outer_Lex.reader(toks)) match {
    32       case Success(spans, rest) if rest.atEnd => spans
    33       case bad => error(bad.toString)
    34     }
    35   }
    36 }