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