1.1 --- a/src/Pure/ROOT	Sat Jul 21 22:13:50 2012 +0200
     1.2 +++ b/src/Pure/ROOT	Sun Jul 22 00:00:22 2012 +0200
     1.3 @@ -20,5 +20,6 @@
     1.4      "ML-Systems/use_context.ML"
     1.5  
     1.6  session Pure in "." =
     1.7 +  theories Pure
     1.8    files "ROOT.ML"  (* FIXME *)
     1.9  

     2.1 --- a/src/Pure/System/build.scala	Sat Jul 21 22:13:50 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Sun Jul 22 00:00:22 2012 +0200
     2.3 @@ -97,8 +97,8 @@
     2.4          new Queue(keys1, graph1)
     2.5        }
     2.6  
     2.7 -      def topological_order: List[(Key, Info)] =
     2.8 -        graph.topological_order.map(key => (key, graph.get_node(key)))
     2.9 +      def topological_order: List[(String, Info)] =
    2.10 +        graph.topological_order.map(key => (key.name, graph.get_node(key)))
    2.11      }
    2.12    }
    2.13  
    2.14 @@ -266,6 +266,44 @@
    2.15    }
    2.16  
    2.17  
    2.18 +  /* dependencies */
    2.19 +
    2.20 +  sealed case class Node(
    2.21 +    loaded_theories: Set[String],
    2.22 +    sources: List[Path])
    2.23 +
    2.24 +  def dependencies(queue: Session.Queue): Map[String, Node] =
    2.25 +    (Map.empty[String, Node] /: queue.topological_order)(
    2.26 +      { case (deps, (name, info)) =>
    2.27 +          val preloaded =
    2.28 +            info.parent match {
    2.29 +              case None => Set.empty[String]
    2.30 +              case Some(parent) => deps(parent).loaded_theories
    2.31 +            }
    2.32 +          val thy_info = new Thy_Info(new Thy_Load(preloaded))
    2.33 +
    2.34 +          val thy_deps =
    2.35 +            thy_info.dependencies(
    2.36 +              info.theories.map(_._2).flatten.
    2.37 +                map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
    2.38 +
    2.39 +          val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
    2.40 +          val sources =
    2.41 +            thy_deps.map({ case (n, h) =>
    2.42 +              val thy = Path.explode(n.node).expand
    2.43 +              val uses =
    2.44 +                h match {
    2.45 +                  case Exn.Res(d) =>
    2.46 +                    d.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
    2.47 +                  case _ => Nil
    2.48 +                }
    2.49 +              thy :: uses
    2.50 +            }).flatten ::: info.files.map(file => info.dir + file)
    2.51 +
    2.52 +          deps + (name -> Node(loaded_theories, sources))
    2.53 +      })
    2.54 +
    2.55 +
    2.56  
    2.57    /** build **/
    2.58  
    2.59 @@ -350,10 +388,8 @@
    2.60  
    2.61      // run jobs
    2.62      val rcs =
    2.63 -      for ((key, info) <- queue.topological_order) yield
    2.64 +      for ((name, info) <- queue.topological_order) yield
    2.65        {
    2.66 -        val name = key.name
    2.67 -
    2.68          if (list_only) { echo(name + " in " + info.dir); 0 }
    2.69          else {
    2.70            val save = build_images || queue.is_inner(name)

     3.1 --- a/src/Pure/System/session.scala	Sat Jul 21 22:13:50 2012 +0200
     3.2 +++ b/src/Pure/System/session.scala	Sun Jul 22 00:00:22 2012 +0200
     3.3 @@ -37,7 +37,7 @@
     3.4  }
     3.5  
     3.6  
     3.7 -class Session(thy_load: Thy_Load = new Thy_Load)
     3.8 +class Session(thy_load: Thy_Load = new Thy_Load())
     3.9  {
    3.10    /* global flags */
    3.11  

     4.1 --- a/src/Pure/Thy/thy_load.scala	Sat Jul 21 22:13:50 2012 +0200
     4.2 +++ b/src/Pure/Thy/thy_load.scala	Sun Jul 22 00:00:22 2012 +0200
     4.3 @@ -10,12 +10,17 @@
     4.4  import java.io.{File => JFile}
     4.5  
     4.6  
     4.7 +object Thy_Load
     4.8 +{
     4.9 +  def thy_path(path: Path): Path = path.ext("thy")
    4.10 +}
    4.11  
    4.12 -class Thy_Load
    4.13 +
    4.14 +class Thy_Load(preloaded: Set[String] = Set.empty)
    4.15  {
    4.16    /* loaded theories provided by prover */
    4.17  
    4.18 -  private var loaded_theories: Set[String] = Set()
    4.19 +  private var loaded_theories: Set[String] = preloaded
    4.20  
    4.21    def register_thy(thy_name: String): Unit =
    4.22      synchronized { loaded_theories += thy_name }
    4.23 @@ -39,15 +44,13 @@
    4.24  
    4.25    /* theory files */
    4.26  
    4.27 -  def thy_path(path: Path): Path = path.ext("thy")
    4.28 -
    4.29    private def import_name(dir: String, s: String): Document.Node.Name =
    4.30    {
    4.31      val theory = Thy_Header.base_name(s)
    4.32      if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
    4.33      else {
    4.34        val path = Path.explode(s)
    4.35 -      val node = append(dir, thy_path(path))
    4.36 +      val node = append(dir, Thy_Load.thy_path(path))
    4.37        val dir1 = append(dir, path.dir)
    4.38        Document.Node.Name(node, dir1, theory)
    4.39      }
    4.40 @@ -60,7 +63,8 @@
    4.41      // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
    4.42      val uses = header.uses
    4.43      if (name.theory != name1)
    4.44 -      error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1))
    4.45 +      error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
    4.46 +        " for theory " + quote(name1))
    4.47      Document.Node.Deps(imports, header.keywords, uses)
    4.48    }
    4.49  

     5.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Sat Jul 21 22:13:50 2012 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Sun Jul 22 00:00:22 2012 +0200
     5.3 @@ -17,7 +17,7 @@
     5.4  import org.gjt.sp.jedit.View
     5.5  
     5.6  
     5.7 -class JEdit_Thy_Load extends Thy_Load
     5.8 +class JEdit_Thy_Load extends Thy_Load()
     5.9  {
    5.10    override def append(dir: String, source_path: Path): String =
    5.11    {