# HG changeset patch
# User wenzelm
# Date 1262705371 -3600
# Node ID b149b70832361d9a20a677d55c672de321cbc993
# Parent  92810c85262e5570f646d57c2e387848ca9db547
separate module Thy_Syntax for command span parsing;

diff -r 92810c85262e -r b149b7083236 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Jan 05 16:29:03 2010 +0100
+++ b/src/Pure/IsaMakefile	Tue Jan 05 16:29:31 2010 +0100
@@ -132,7 +132,7 @@
   System/isabelle_system.scala System/platform.scala			\
   System/session_manager.scala System/standard_system.scala		\
   Thy/completion.scala Thy/html.scala Thy/thy_header.scala		\
-  library.scala
+  Thy/thy_syntax.scala library.scala
 
 JAR_DIR = $(ISABELLE_HOME)/lib/classes
 PURE_JAR = $(JAR_DIR)/Pure.jar
diff -r 92810c85262e -r b149b7083236 src/Pure/Isar/outer_parse.scala
--- a/src/Pure/Isar/outer_parse.scala	Tue Jan 05 16:29:03 2010 +0100
+++ b/src/Pure/Isar/outer_parse.scala	Tue Jan 05 16:29:31 2010 +0100
@@ -68,17 +68,6 @@
     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)
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)
+    }
+  }
+}