clarified signature: Known.theories retains Document.Node.Entry (with header);

--- a/src/Pure/PIDE/command.scala	Mon May 28 13:35:43 2018 +0200
+++ b/src/Pure/PIDE/command.scala	Mon May 28 17:40:34 2018 +0200
@@ -511,7 +511,7 @@
                 val qualifier = resources.session_base.theory_qualifier(node_name)
                 val dir = node_name.master_dir
                 for {
-                  (_, known_name) <- resources.session_base.known.theories.toList
+                  known_name <- resources.session_base.known.theory_names
                   if completed(known_name.theory_base_name)
                 }
                 yield {

--- a/src/Pure/PIDE/document.scala	Mon May 28 13:35:43 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Mon May 28 17:40:34 2018 +0200
@@ -137,6 +137,8 @@
 
     sealed case class Entry(name: Node.Name, header: Node.Header)
     {
+      def map(f: String => String): Entry = copy(name = name.map(f))
+
       override def toString: String = name.toString
     }
 

--- a/src/Pure/PIDE/resources.scala	Mon May 28 13:35:43 2018 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon May 28 17:40:34 2018 +0200
@@ -277,7 +277,7 @@
         loaded_theories.all_preds(theories.map(_.theory)).
           filter(session_base.loaded_theories.defined(_))
 
-      base_theories.map(theory => session_base.known.theories(theory).path) :::
+      base_theories.map(theory => session_base.known.theories(theory).name.path) :::
       base_theories.flatMap(session_base.known.loaded_files(_))
     }
 

--- a/src/Pure/Thy/sessions.scala	Mon May 28 13:35:43 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon May 28 17:40:34 2018 +0200
@@ -41,42 +41,45 @@
 
     def make(local_dir: Path, bases: List[Base],
       sessions: List[(String, Position.T)] = Nil,
-      theories: List[Document.Node.Name] = Nil,
+      theories: List[Document.Node.Entry] = Nil,
       loaded_files: List[(String, List[Path])] = Nil): Known =
     {
       def bases_iterator(local: Boolean) =
         for {
           base <- bases.iterator
-          (_, name) <- (if (local) base.known.theories_local else base.known.theories).iterator
-        } yield name
+          (_, entry) <- (if (local) base.known.theories_local else base.known.theories).iterator
+        } yield entry
 
       def local_theories_iterator =
       {
         val local_path = local_dir.canonical_file.toPath
-        theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path))
+        theories.iterator.filter(entry =>
+          entry.name.path.canonical_file.toPath.startsWith(local_path))
       }
 
       val known_sessions =
         (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions })
 
       val known_theories =
-        (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({
-          case (known, name) =>
-            known.get(name.theory) match {
-              case Some(name1) if name != name1 =>
-                error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
-              case _ => known + (name.theory -> name)
+        (Map.empty[String, Document.Node.Entry] /: (bases_iterator(false) ++ theories.iterator))({
+          case (known, entry) =>
+            known.get(entry.name.theory) match {
+              case Some(entry1) if entry.name != entry1.name =>
+                error("Duplicate theory " + quote(entry.name.node) + " vs. " +
+                  quote(entry1.name.node))
+              case _ => known + (entry.name.theory -> entry)
             }
           })
       val known_theories_local =
-        (Map.empty[String, Document.Node.Name] /:
+        (Map.empty[String, Document.Node.Entry] /:
             (bases_iterator(true) ++ local_theories_iterator))({
-          case (known, name) => known + (name.theory -> name)
+          case (known, entry) => known + (entry.name.theory -> entry)
         })
       val known_files =
         (Map.empty[JFile, List[Document.Node.Name]] /:
             (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
-          case (known, name) =>
+          case (known, entry) =>
+            val name = entry.name
             val file = name.path.canonical_file
             val theories1 = known.getOrElse(file, Nil)
             if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
@@ -89,7 +92,8 @@
 
       Known(
         known_sessions,
-        known_theories, known_theories_local,
+        known_theories,
+        known_theories_local,
         known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
         known_loaded_files)
     }
@@ -97,8 +101,8 @@
 
   sealed case class Known(
     sessions: Map[String, Position.T] = Map.empty,
-    theories: Map[String, Document.Node.Name] = Map.empty,
-    theories_local: Map[String, Document.Node.Name] = Map.empty,
+    theories: Map[String, Document.Node.Entry] = Map.empty,
+    theories_local: Map[String, Document.Node.Entry] = Map.empty,
     files: Map[JFile, List[Document.Node.Name]] = Map.empty,
     loaded_files: Map[String, List[Path]] = Map.empty)
   {
@@ -112,6 +116,25 @@
         theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))),
         files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_)))))
 
+    def theory_names: List[Document.Node.Name] = theories.iterator.map(p => p._2.name).toList
+
+    lazy val theory_graph: Graph[Document.Node.Name, Unit] =
+    {
+      val graph0 =
+        (Graph.empty[Document.Node.Name, Unit](Document.Node.Name.Ordering) /: theories)(
+          {
+            case (g1, (_, entry)) =>
+              (g1.default_node(entry.name, ()) /: entry.header.imports)(
+                { case (g2, (parent, _)) => g2.default_node(parent, ()) })
+          })
+      (graph0 /: theories)(
+        {
+          case (g1, (_, entry)) =>
+            (g1 /: entry.header.imports)(
+              { case (g2, (parent, _)) => g2.add_edge(parent, entry.name) })
+        })
+    }
+
     def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
     {
       val res = files.getOrElse(File.canonical(file), Nil).headOption
@@ -159,11 +182,11 @@
       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
 
     def known_theory(name: String): Option[Document.Node.Name] =
-      known.theories.get(name)
+      known.theories.get(name).map(_.name)
 
     def dest_known_theories: List[(String, String)] =
-      for ((theory, node_name) <- known.theories.toList)
-        yield (theory, node_name.node)
+      for ((theory, entry) <- known.theories.toList)
+        yield (theory, entry.name.node)
 
     def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
   }
@@ -319,7 +342,7 @@
             val known =
               Known.make(info.dir, List(imports_base),
                 sessions = List(info.name -> info.pos),
-                theories = dependencies.theories,
+                theories = dependencies.entries,
                 loaded_files = loaded_files)
 
             val sources_errors =

--- a/src/Pure/Tools/imports.scala	Mon May 28 13:35:43 2018 +0200
+++ b/src/Pure/Tools/imports.scala	Mon May 28 17:40:34 2018 +0200
@@ -117,7 +117,7 @@
 
             val extra_imports =
               (for {
-                (_, a) <- session_base.known.theories.iterator
+                a <- session_base.known.theory_names
                 if session_base.theory_qualifier(a) == info.name
                 b <- deps.all_known.get_file(a.path.file)
                 qualifier = session_base.theory_qualifier(b)
@@ -127,7 +127,7 @@
             val loaded_imports =
               deps.sessions_structure.imports_requirements(
                 session_base.loaded_theories.keys.map(a =>
-                  session_base.theory_qualifier(session_base.known.theories(a))))
+                  session_base.theory_qualifier(session_base.known.theories(a).name)))
               .toSet - session_name
 
             val minimal_imports =
@@ -188,13 +188,13 @@
               } yield upd
 
             val updates_theories =
-              for {
-                (_, name) <- session_base.known.theories_local.toList
+              (for {
+                name <- session_base.known.theories_local.iterator.map(p => p._2.name)
                 if session_base.theory_qualifier(name) == info.name
                 (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
                 upd <- update_name(session_base.overall_syntax.keywords, pos,
                   standard_import(session_base.theory_qualifier(name), name.master_dir, _))
-              } yield upd
+              } yield upd).toList
 
             updates_root ::: updates_theories
           })