find files via load commands within theory text;
clarified Thy_Load.with_thy_text, simplified Thy_Load.check_thy;

--- a/src/Pure/Isar/outer_syntax.scala	Wed Aug 22 16:24:52 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Aug 22 18:04:30 2012 +0200
@@ -58,8 +58,8 @@
   def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
   def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
 
-  def thy_load_commands: List[String] =
-    (for ((name, (Keyword.THY_LOAD, _)) <- keywords.iterator) yield name).toList
+  def thy_load_commands: List[(String, List[String])] =
+    (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
 
   def + (name: String, kind: (String, List[String]), replace: String): Outer_Syntax =
     new Outer_Syntax(

--- a/src/Pure/Thy/thy_info.scala	Wed Aug 22 16:24:52 2012 +0200
+++ b/src/Pure/Thy/thy_info.scala	Wed Aug 22 18:04:30 2012 +0200
@@ -64,7 +64,7 @@
         if (initiators.contains(name)) error(cycle_msg(initiators))
         val syntax = required.make_syntax
         val header =
-          try { thy_load.check_thy(syntax, name) }
+          try { thy_load.check_thy_files(syntax, name) }
           catch {
             case ERROR(msg) =>
               cat_error(msg, "The error(s) above occurred while examining theory " +

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

--- a/src/Tools/jEdit/src/document_model.scala	Wed Aug 22 16:24:52 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Aug 22 18:04:30 2012 +0200
@@ -68,8 +68,7 @@
     Swing_Thread.require()
     Isabelle.buffer_lock(buffer) {
       Exn.capture {
-        val text = buffer.getSegment(0, buffer.getLength)
-        Isabelle.thy_load.check_thy_text(session.recent_syntax, name, text)
+        Isabelle.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
       } match {
         case Exn.Res(header) => header
         case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))

--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Aug 22 16:24:52 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Aug 22 18:04:30 2012 +0200
@@ -33,6 +33,23 @@
     }
   }
 
+  override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
+  {
+    Swing_Thread.now {
+      Isabelle.jedit_buffer(name.node) match {
+        case Some(buffer) =>
+          Isabelle.buffer_lock(buffer) {
+            Some(f(buffer.getSegment(0, buffer.getLength)))
+          }
+        case None => None
+      }
+    } getOrElse {
+      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
+      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
+      f(File.read(file))
+    }
+  }
+
   def check_file(view: View, path: String): Boolean =
   {
     val vfs = VFSManager.getVFSForPath(path)
@@ -52,23 +69,5 @@
       catch { case _: IOException => }
     }
   }
-
-  override def check_thy(syntax: Outer_Syntax, name: Document.Node.Name)
-    : Document.Node.Header =
-  {
-    Swing_Thread.now {
-      Isabelle.jedit_buffer(name.node) match {
-        case Some(buffer) =>
-          Isabelle.buffer_lock(buffer) {
-            Some(check_thy_text(syntax, name, buffer.getSegment(0, buffer.getLength)))
-          }
-        case None => None
-      }
-    } getOrElse {
-      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
-      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
-      check_thy_text(syntax, name, File.read(file))
-    }
-  }
 }