src/Pure/Thy/thy_load.scala

--- a/src/Pure/Thy/thy_load.scala	Wed Aug 22 16:24:52 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Wed Aug 22 18:04:30 2012 +0200
@@ -7,6 +7,8 @@
 package isabelle
 
 
+import scala.annotation.tailrec
+
 import java.io.{File => JFile}
 
 
@@ -27,6 +29,13 @@
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode
 
+  def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
+  {
+    val path = Path.explode(name.node)
+    if (!path.is_file) error("No such file: " + path.toString)
+    f(File.read(path))
+  }
+
 
   /* theory files */
 
@@ -42,26 +51,65 @@
     }
   }
 
-  def check_thy_text(syntax: Outer_Syntax, name: Document.Node.Name, text: CharSequence)
-    : Document.Node.Header =
+  private def find_file(tokens: List[Token]): Option[String] =
+  {
+    def clean(toks: List[Token]): List[Token] =
+      toks match {
+        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
+        case t :: ts => t :: clean(ts)
+        case Nil => Nil
+      }
+    val clean_tokens = clean(tokens.filter(_.is_proper))
+    clean_tokens.reverse.find(_.is_name).map(_.content)
+  }
+
+  def find_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) })) {
+      val spans = Thy_Syntax.parse_spans(syntax.scan(text))
+      spans.iterator.map({
+        case toks @ (tok :: _) if tok.is_command =>
+          thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
+            case Some((_, exts)) =>
+              find_file(toks) match {
+                case Some(file) =>
+                  if (exts.isEmpty) List(file)
+                  else exts.map(ext => file + "." + ext)
+                case None => Nil
+              }
+            case None => Nil
+          }
+        case _ => Nil
+      }).flatten.toList
+    }
+    else Nil
+  }
+
+  def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
   {
     val header = Thy_Header.read(text)
+
     val name1 = header.name
-    val imports = header.imports.map(import_name(name.dir, _))
-    // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
-    // FIXME find files in text
-    val uses = header.uses
     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)
   }
 
-  def check_thy(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header =
-  {
-    val path = Path.explode(name.node)
-    if (!path.is_file) error("No such file: " + path.toString)
-    check_thy_text(syntax, name, File.read(path))
-  }
+  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, string)
+        header.copy(uses = header.uses ::: more_uses.map((_, false)))
+      })
 }