diff -r 92810c85262e -r b149b7083236 src/Pure/Thy/thy_syntax.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Jan 05 16:29:31 2010 +0100
@@ -0,0 +1,36 @@
+/*  Title:      Pure/Thy/thy_syntax.scala
+    Author:     Makarius
+
+Superficial theory syntax: command spans.
+*/
+
+package isabelle
+
+
+class Thy_Syntax
+{
+  private val parser = new Outer_Parse.Parser
+  {
+    override def filter_proper = false
+
+    val command_span: Parser[Span] =
+    {
+      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)
+    }
+  }
+
+  type Span = List[Outer_Lex.Token]
+
+  def parse_spans(toks: List[Outer_Lex.Token]): List[Span] =
+  {
+    import parser._
+
+    parse(rep(command_span), Outer_Lex.reader(toks)) match {
+      case Success(spans, rest) if rest.atEnd => spans
+      case bad => error(bad.toString)
+    }
+  }
+}