# HG changeset patch
# User wenzelm
# Date 1309454649 -7200
# Node ID 21a57a0c5f2557ea59495aaeb05aaa379f1d1630
# Parent  16482dc641d471bc84e6714a25f757f79f41522a
more general theory header parsing;

diff -r 16482dc641d4 -r 21a57a0c5f25 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Thu Jun 30 16:50:26 2011 +0200
+++ b/src/Pure/Isar/token.scala	Thu Jun 30 19:24:09 2011 +0200
@@ -81,6 +81,9 @@
   def is_comment: Boolean = kind == Token.Kind.COMMENT
   def is_ignored: Boolean = is_space || is_comment
 
+  def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin"
+  def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end"
+
   def content: String =
     if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
     else if (kind == Token.Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)
diff -r 16482dc641d4 -r 21a57a0c5f25 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Thu Jun 30 16:50:26 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Thu Jun 30 19:24:09 2011 +0200
@@ -7,8 +7,9 @@
 package isabelle
 
 
+import scala.annotation.tailrec
 import scala.collection.mutable
-import scala.util.parsing.input.{Reader, CharSequenceReader}
+import scala.util.parsing.input.Reader
 import scala.util.matching.Regex
 
 import java.io.File
@@ -25,6 +26,12 @@
   val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
 
   final case class Header(val name: String, val imports: List[String], val uses: List[String])
+  {
+    def decode_permissive_utf8: Header =
+      Header(Standard_System.decode_permissive_utf8(name),
+        imports.map(Standard_System.decode_permissive_utf8),
+        uses.map(Standard_System.decode_permissive_utf8))
+  }
 
 
   /* file name */
@@ -50,8 +57,8 @@
 
   val header: Parser[Header] =
   {
-    val file_name = atom("file name", _.is_name) ^^ Standard_System.decode_permissive_utf8
-    val theory_name = atom("theory name", _.is_name) ^^ Standard_System.decode_permissive_utf8
+    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
@@ -70,27 +77,32 @@
 
   /* read -- lazy scanning */
 
-  def read(file: File): Header =
+  def read(reader: Reader[Char]): Header =
   {
     val token = lexicon.token(symbols, _ => false)
     val toks = new mutable.ListBuffer[Token]
 
-    def scan_to_begin(in: Reader[Char])
+    @tailrec def scan_to_begin(in: Reader[Char])
     {
       token(in) match {
         case lexicon.Success(tok, rest) =>
           toks += tok
-          if (!(tok.kind == Token.Kind.KEYWORD && tok.content == BEGIN))
-            scan_to_begin(rest)
+          if (!tok.is_begin) scan_to_begin(rest)
         case _ =>
       }
     }
-    val reader = Scan.byte_reader(file)
-    try { scan_to_begin(reader) } finally { reader.close }
+    scan_to_begin(reader)
 
     parse(commit(header), Token.reader(toks.toList)) match {
       case Success(result, _) => result
       case bad => error(bad.toString)
     }
   }
+
+  def read(file: File): Header =
+  {
+    val reader = Scan.byte_reader(file)
+    try { read(reader).decode_permissive_utf8 }
+    finally { reader.close }
+  }
 }