src/Pure/Thy/thy_load.scala

--- a/src/Pure/Thy/thy_load.scala	Thu Dec 06 23:07:10 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala	Fri Dec 07 13:38:32 2012 +0100
@@ -80,7 +80,7 @@
     clean_tokens.reverse.find(_.is_name).map(_.content)
   }
 
-  def find_files(syntax: Outer_Syntax, text: String): List[String] =
+  def theory_body_files(syntax: Outer_Syntax, text: String): List[String] =
   {
     val thy_load_commands = syntax.thy_load_commands
     if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
@@ -105,28 +105,22 @@
 
   def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
   {
-    val header = Thy_Header.read(text)
+    try {
+      val header = Thy_Header.read(text)
 
-    val name1 = header.name
-    if (name.theory != name1)
-      error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
-        " for theory " + quote(name1))
+      val name1 = header.name
+      if (name.theory != name1)
+        error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
+          " for theory " + quote(name1))
 
-    val imports = header.imports.map(import_name(name.dir, _))
-    val uses = header.uses
-    Document.Node.Header(imports, header.keywords, uses)
+      val imports = header.imports.map(import_name(name.dir, _))
+      val uses = header.uses
+      Document.Node.Header(imports, header.keywords, uses)
+    }
+    catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) }
   }
 
   def check_thy(name: Document.Node.Name): Document.Node.Header =
     with_thy_text(name, check_thy_text(name, _))
-
-  def check_thy_files(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header =
-    with_thy_text(name, text =>
-      {
-        val string = text.toString
-        val header = check_thy_text(name, string)
-        val more_uses = find_files(syntax.add_keywords(header.keywords), string)
-        header.copy(uses = header.uses ::: more_uses.map((_, false)))
-      })
 }