src/Pure/Thy/thy_info.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_info.scala	Mon Jul 04 16:27:11 2011 +0200
@@ -0,0 +1,59 @@
+/*  Title:      Pure/Thy/thy_info.scala
+    Author:     Makarius
+
+Theory and file dependencies.
+*/
+
+package isabelle
+
+
+class Thy_Info(thy_load: Thy_Load)
+{
+  /* messages */
+
+  private def show_path(names: List[String]): String =
+    names.map(Library.quote).mkString(" via ")
+
+  private def cycle_msg(names: List[String]): String =
+    "Cyclic dependency of " + show_path(names)
+
+  private def required_by(s: String, initiators: List[String]): String =
+    if (initiators.isEmpty) ""
+    else s + "(required by " + show_path(initiators.reverse) + ")"
+
+
+  /* dependencies */
+
+  type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
+
+  private def require_thys(
+      initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
+    (deps /: strs)(require_thy(initiators, dir, _, _))
+
+  private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
+  {
+    val path = Path.explode(str)
+    val name = path.base.implode
+
+    if (deps.isDefinedAt(name)) deps
+    else {
+      val dir1 = dir + path.dir
+      try {
+        if (initiators.contains(name)) error(cycle_msg(initiators))
+        val (text, header) =
+          try { thy_load.check_thy(dir1, name) }
+          catch {
+            case ERROR(msg) =>
+              cat_error(msg, "The error(s) above occurred while examining theory " +
+                Library.quote(name) + required_by("\n", initiators))
+          }
+        require_thys(name :: initiators, dir1,
+          deps + (name -> Exn.Res(text, header)), header.imports)
+      }
+      catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
+    }
+  }
+
+  def dependencies(dir: Path, str: String): Deps =
+    require_thy(Nil, dir, Map.empty, str)  // FIXME capture errors in str (!??)
+}