--- a/src/Pure/Isar/outer_parse.scala Tue Jan 05 15:44:32 2010 +0100
+++ b/src/Pure/Isar/outer_parse.scala Tue Jan 05 15:45:32 2010 +0100
@@ -17,8 +17,10 @@
{
type Elem = Outer_Lex.Token
+ def filter_proper = true
+
private def proper(in: Input): Input =
- if (in.atEnd || in.first.is_proper) in
+ if (in.atEnd || in.first.is_proper || !filter_proper) in
else proper(in.rest)
def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
@@ -41,11 +43,12 @@
}
}
+ def not_eof: Parser[Elem] = token("input token", _ => true)
+ def eof: Parser[Unit] = not(not_eof)
+
def atom(s: String, pred: Elem => Boolean): Parser[String] =
token(s, pred) ^^ (_.content)
- def not_eof: Parser[Elem] = token("input token", _ => true)
-
def keyword(name: String): Parser[String] =
atom(Outer_Lex.Token_Kind.KEYWORD.toString + " \"" + name + "\"",
tok => tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == name)
@@ -65,6 +68,17 @@
def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
+ /* command spans */
+
+ def command_span: Parser[List[Elem]] =
+ {
+ val whitespace = token("white space", tok => tok.is_space || tok.is_comment)
+ val command = token("command keyword", _.is_command)
+ val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof
+ command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body)
+ }
+
+
/* wrappers */
def parse[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = p(in)