# HG changeset patch
# User wenzelm
# Date 1261514897 -3600
# Node ID 7501b2910900dd98286863b19400a9b535006efe
# Parent  18843829c7f2579a2296225c134193e8e5b1f599
basic setup for header scanning/parsing;

diff -r 18843829c7f2 -r 7501b2910900 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Dec 22 21:47:27 2009 +0100
+++ b/src/Pure/Thy/thy_header.scala	Tue Dec 22 21:48:17 2009 +0100
@@ -1,12 +1,16 @@
 /*  Title:      Pure/Thy/thy_header.scala
     Author:     Makarius
 
-Theory header keywords.
+Theory headers -- independent of outer syntax.
 */
 
 package isabelle
 
 
+import scala.collection.mutable
+import scala.util.parsing.input.{Reader, CharSequenceReader}
+
+
 object Thy_Header
 {
   val HEADER = "header"
@@ -15,5 +19,54 @@
   val USES = "uses"
   val BEGIN = "begin"
 
-  val keywords = List("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
+  val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
 }
+
+
+class Thy_Header(symbols: Symbol.Interpretation) extends Outer_Parse.Parser
+{
+  import Thy_Header._
+
+
+  /* header */
+
+  val header: Parser[(String, List[String], List[String])] =
+  {
+    val file_name = atom("file name", _.is_name)
+    val theory_name = atom("theory name", _.is_name)
+
+    val file =
+      keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name
+
+    val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }
+
+    val args =
+      theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^
+        { case x ~ (_ ~ (ys ~ zs ~ _)) => (x, ys, zs) }
+
+    (keyword(HEADER) ~ tags) ~!
+      ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
+    (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
+  }
+
+
+  /* scan -- lazy approximation */
+
+  def scan(text: CharSequence): List[Outer_Lex.Token] =
+  {
+    val token = lexicon.token(symbols, _ => false)
+    val toks = new mutable.ListBuffer[Outer_Lex.Token]
+    def scan_until_begin(in: Reader[Char])
+    {
+      token(in) match {
+        case lexicon.Success(tok, rest) =>
+          toks += tok
+          if (!(tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == BEGIN))
+            scan_until_begin(rest)
+        case _ =>
+      }
+    }
+    scan_until_begin(new CharSequenceReader(text))
+    toks.toList
+  }
+}