# HG changeset patch
# User wenzelm
# Date 1262702732 -3600
# Node ID bfe8d699873492e20bfa016d1a37f09392efdf16
# Parent  dc932fc1b9063676b39ded67a1619aef7035b5f0
added filter_proper parameter;
added eof;
added command_span;

diff -r dc932fc1b906 -r bfe8d6998734 src/Pure/Isar/outer_parse.scala
--- 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)