# HG changeset patch
# User wenzelm
# Date 1342908022 -7200
# Node ID 9613780a805bcc28ade8f8dea0258a0409cb1591
# Parent  c4d337782de4b2bca615b20c0f3f3ca161338f85
determine source dependencies, relatively to preloaded theories;
tuned signature;

diff -r c4d337782de4 -r 9613780a805b src/Pure/ROOT
--- a/src/Pure/ROOT	Sat Jul 21 22:13:50 2012 +0200
+++ b/src/Pure/ROOT	Sun Jul 22 00:00:22 2012 +0200
@@ -20,5 +20,6 @@
     "ML-Systems/use_context.ML"
 
 session Pure in "." =
+  theories Pure
   files "ROOT.ML"  (* FIXME *)
 
diff -r c4d337782de4 -r 9613780a805b src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Sat Jul 21 22:13:50 2012 +0200
+++ b/src/Pure/System/build.scala	Sun Jul 22 00:00:22 2012 +0200
@@ -97,8 +97,8 @@
         new Queue(keys1, graph1)
       }
 
-      def topological_order: List[(Key, Info)] =
-        graph.topological_order.map(key => (key, graph.get_node(key)))
+      def topological_order: List[(String, Info)] =
+        graph.topological_order.map(key => (key.name, graph.get_node(key)))
     }
   }
 
@@ -266,6 +266,44 @@
   }
 
 
+  /* dependencies */
+
+  sealed case class Node(
+    loaded_theories: Set[String],
+    sources: List[Path])
+
+  def dependencies(queue: Session.Queue): Map[String, Node] =
+    (Map.empty[String, Node] /: queue.topological_order)(
+      { case (deps, (name, info)) =>
+          val preloaded =
+            info.parent match {
+              case None => Set.empty[String]
+              case Some(parent) => deps(parent).loaded_theories
+            }
+          val thy_info = new Thy_Info(new Thy_Load(preloaded))
+
+          val thy_deps =
+            thy_info.dependencies(
+              info.theories.map(_._2).flatten.
+                map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
+
+          val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
+          val sources =
+            thy_deps.map({ case (n, h) =>
+              val thy = Path.explode(n.node).expand
+              val uses =
+                h match {
+                  case Exn.Res(d) =>
+                    d.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
+                  case _ => Nil
+                }
+              thy :: uses
+            }).flatten ::: info.files.map(file => info.dir + file)
+
+          deps + (name -> Node(loaded_theories, sources))
+      })
+
+
 
   /** build **/
 
@@ -350,10 +388,8 @@
 
     // run jobs
     val rcs =
-      for ((key, info) <- queue.topological_order) yield
+      for ((name, info) <- queue.topological_order) yield
       {
-        val name = key.name
-
         if (list_only) { echo(name + " in " + info.dir); 0 }
         else {
           val save = build_images || queue.is_inner(name)
diff -r c4d337782de4 -r 9613780a805b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Jul 21 22:13:50 2012 +0200
+++ b/src/Pure/System/session.scala	Sun Jul 22 00:00:22 2012 +0200
@@ -37,7 +37,7 @@
 }
 
 
-class Session(thy_load: Thy_Load = new Thy_Load)
+class Session(thy_load: Thy_Load = new Thy_Load())
 {
   /* global flags */
 
diff -r c4d337782de4 -r 9613780a805b src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Sat Jul 21 22:13:50 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Sun Jul 22 00:00:22 2012 +0200
@@ -10,12 +10,17 @@
 import java.io.{File => JFile}
 
 
+object Thy_Load
+{
+  def thy_path(path: Path): Path = path.ext("thy")
+}
 
-class Thy_Load
+
+class Thy_Load(preloaded: Set[String] = Set.empty)
 {
   /* loaded theories provided by prover */
 
-  private var loaded_theories: Set[String] = Set()
+  private var loaded_theories: Set[String] = preloaded
 
   def register_thy(thy_name: String): Unit =
     synchronized { loaded_theories += thy_name }
@@ -39,15 +44,13 @@
 
   /* theory files */
 
-  def thy_path(path: Path): Path = path.ext("thy")
-
   private def import_name(dir: String, s: String): Document.Node.Name =
   {
     val theory = Thy_Header.base_name(s)
     if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
     else {
       val path = Path.explode(s)
-      val node = append(dir, thy_path(path))
+      val node = append(dir, Thy_Load.thy_path(path))
       val dir1 = append(dir, path.dir)
       Document.Node.Name(node, dir1, theory)
     }
@@ -60,7 +63,8 @@
     // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
     val uses = header.uses
     if (name.theory != name1)
-      error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1))
+      error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
+        " for theory " + quote(name1))
     Document.Node.Deps(imports, header.keywords, uses)
   }
 
diff -r c4d337782de4 -r 9613780a805b src/Tools/jEdit/src/jedit_thy_load.scala
--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Sat Jul 21 22:13:50 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Sun Jul 22 00:00:22 2012 +0200
@@ -17,7 +17,7 @@
 import org.gjt.sp.jedit.View
 
 
-class JEdit_Thy_Load extends Thy_Load
+class JEdit_Thy_Load extends Thy_Load()
 {
   override def append(dir: String, source_path: Path): String =
   {