separate module Thy_Syntax for command span parsing;
authorwenzelm
Tue Jan 05 16:29:31 2010 +0100 (2010-01-05)
changeset 34268b149b7083236
parent 34267 92810c85262e
child 34274 2cb69632d3fa
separate module Thy_Syntax for command span parsing;
src/Pure/IsaMakefile
src/Pure/Isar/outer_parse.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/IsaMakefile	Tue Jan 05 16:29:03 2010 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Tue Jan 05 16:29:31 2010 +0100
     1.3 @@ -132,7 +132,7 @@
     1.4    System/isabelle_system.scala System/platform.scala			\
     1.5    System/session_manager.scala System/standard_system.scala		\
     1.6    Thy/completion.scala Thy/html.scala Thy/thy_header.scala		\
     1.7 -  library.scala
     1.8 +  Thy/thy_syntax.scala library.scala
     1.9  
    1.10  JAR_DIR = $(ISABELLE_HOME)/lib/classes
    1.11  PURE_JAR = $(JAR_DIR)/Pure.jar
     2.1 --- a/src/Pure/Isar/outer_parse.scala	Tue Jan 05 16:29:03 2010 +0100
     2.2 +++ b/src/Pure/Isar/outer_parse.scala	Tue Jan 05 16:29:31 2010 +0100
     2.3 @@ -68,17 +68,6 @@
     2.4      def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
     2.5  
     2.6  
     2.7 -    /* command spans */
     2.8 -
     2.9 -    def command_span: Parser[List[Elem]] =
    2.10 -    {
    2.11 -      val whitespace = token("white space", tok => tok.is_space || tok.is_comment)
    2.12 -      val command = token("command keyword", _.is_command)
    2.13 -      val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof
    2.14 -      command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body)
    2.15 -    }
    2.16 -
    2.17 -
    2.18      /* wrappers */
    2.19  
    2.20      def parse[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = p(in)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Jan 05 16:29:31 2010 +0100
     3.3 @@ -0,0 +1,36 @@
     3.4 +/*  Title:      Pure/Thy/thy_syntax.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Superficial theory syntax: command spans.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +class Thy_Syntax
    3.14 +{
    3.15 +  private val parser = new Outer_Parse.Parser
    3.16 +  {
    3.17 +    override def filter_proper = false
    3.18 +
    3.19 +    val command_span: Parser[Span] =
    3.20 +    {
    3.21 +      val whitespace = token("white space", tok => tok.is_space || tok.is_comment)
    3.22 +      val command = token("command keyword", _.is_command)
    3.23 +      val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof
    3.24 +      command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body)
    3.25 +    }
    3.26 +  }
    3.27 +
    3.28 +  type Span = List[Outer_Lex.Token]
    3.29 +
    3.30 +  def parse_spans(toks: List[Outer_Lex.Token]): List[Span] =
    3.31 +  {
    3.32 +    import parser._
    3.33 +
    3.34 +    parse(rep(command_span), Outer_Lex.reader(toks)) match {
    3.35 +      case Success(spans, rest) if rest.atEnd => spans
    3.36 +      case bad => error(bad.toString)
    3.37 +    }
    3.38 +  }
    3.39 +}