--- 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
--- 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)
--- /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)
+ }
+ }
+}