src/Pure/PIDE/resources.scala

--- a/src/Pure/PIDE/resources.scala	Tue Oct 31 15:36:50 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Oct 31 15:55:50 2017 +0100
@@ -17,7 +17,7 @@
   val session_base: Sessions.Base,
   val log: Logger = No_Logger)
 {
-  val thy_info = new Thy_Info(this)
+  resources =>
 
   def thy_path(path: Path): Path = path.ext("thy")
 
@@ -213,7 +213,113 @@
       previous: Document.Version,
       doc_blobs: Document.Blobs,
       edits: List[Document.Edit_Text]): Session.Change =
-    Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
+    Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits)
 
   def commit(change: Session.Change) { }
+
+
+  /* theory and file dependencies */
+
+  object Dependencies
+  {
+    val empty = new Dependencies(Nil, Set.empty)
+  }
+
+  final class Dependencies private(
+    rev_entries: List[Document.Node.Entry],
+    val seen: Set[Document.Node.Name])
+  {
+    def :: (entry: Document.Node.Entry): Dependencies =
+      new Dependencies(entry :: rev_entries, seen)
+
+    def + (name: Document.Node.Name): Dependencies =
+      new Dependencies(rev_entries, seen + name)
+
+    def entries: List[Document.Node.Entry] = rev_entries.reverse
+    def names: List[Document.Node.Name] = entries.map(_.name)
+
+    def errors: List[String] = entries.flatMap(_.header.errors)
+
+    lazy val loaded_theories: Graph[String, Outer_Syntax] =
+      (session_base.loaded_theories /: entries)({ case (graph, entry) =>
+        val name = entry.name.theory
+        val imports = entry.header.imports.map(p => p._1.theory)
+
+        val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
+        val graph2 = (graph1 /: imports)(_.add_edge(_, name))
+
+        val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
+        val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node(_))
+        val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
+
+        graph2.map_node(name, _ => syntax)
+      })
+
+    def loaded_files: List[(String, List[Path])] =
+    {
+      names.map(_.theory) zip
+        Par_List.map((e: () => List[Path]) => e(),
+          names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
+    }
+
+    def imported_files: List[Path] =
+    {
+      val base_theories =
+        loaded_theories.all_preds(names.map(_.theory)).
+          filter(session_base.loaded_theories.defined(_))
+
+      base_theories.map(theory => session_base.known.theories(theory).path) :::
+      base_theories.flatMap(session_base.known.loaded_files(_))
+    }
+
+    lazy val overall_syntax: Outer_Syntax =
+      Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
+
+    override def toString: String = entries.toString
+  }
+
+  private def show_path(names: List[Document.Node.Name]): String =
+    names.map(name => quote(name.theory)).mkString(" via ")
+
+  private def cycle_msg(names: List[Document.Node.Name]): String =
+    "Cyclic dependency of " + show_path(names)
+
+  private def required_by(initiators: List[Document.Node.Name]): String =
+    if (initiators.isEmpty) ""
+    else "\n(required by " + show_path(initiators.reverse) + ")"
+
+  private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
+    thy: (Document.Node.Name, Position.T)): Dependencies =
+  {
+    val (name, pos) = thy
+
+    def message: String =
+      "The error(s) above occurred for theory " + quote(name.theory) +
+        required_by(initiators) + Position.here(pos)
+
+    val required1 = required + name
+    if (required.seen(name)) required
+    else if (session_base.loaded_theory(name)) required1
+    else {
+      try {
+        if (initiators.contains(name)) error(cycle_msg(initiators))
+        val header =
+          try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
+          catch { case ERROR(msg) => cat_error(msg, message) }
+        Document.Node.Entry(name, header) ::
+          require_thys(name :: initiators, required1, header.imports)
+      }
+      catch {
+        case e: Throwable =>
+          Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
+      }
+    }
+  }
+
+  private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
+      thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+    (required /: thys)(require_thy(initiators, _, _))
+
+  def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+    require_thys(Nil, Dependencies.empty, thys)
 }