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