merged

--- a/src/Pure/Admin/afp.scala	Tue Oct 10 17:15:37 2017 +0100
+++ b/src/Pure/Admin/afp.scala	Tue Oct 10 19:51:54 2017 +0200
@@ -43,23 +43,34 @@
   private def sessions_deps(entry: AFP.Entry): List[String] =
     entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted
 
-  val entries_graph: Graph[String, Unit] =
+  def dependency_graph(acyclic: Boolean): Graph[String, Unit] =
   {
     val session_entries =
-      (Multi_Map.empty[String, String] /: entries) { case (m1, e) =>
-        (m1 /: e.sessions) { case (m2, s) => m2.insert(s, e.name) }
+      (Map.empty[String, String] /: entries) {
+        case (m1, e) => (m1 /: e.sessions) { case (m2, s) => m2 + (s -> e.name) }
       }
-    (Graph.empty[String, Unit] /: entries) { case (g, e1) =>
-      val name1 = e1.name
-      val g1 = g.default_node(name1, ())
-      (g1 /: sessions_deps(e1)) { case (g2, s2) =>
-        (g2 /: session_entries.get_list(s2)) { case (g3, name2) =>
-          if (name1 == name2) g3 else g3.default_node(name2, ()).add_edge(name2, name1)
+    (Graph.empty[String, Unit] /: entries) { case (g, entry) =>
+      val e1 = entry.name
+      (g.default_node(e1, ()) /: sessions_deps(entry)) { case (g1, s) =>
+        (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
+          val g3 = g2.default_node(e2, ())
+          if (acyclic) {
+            try { g3.add_edge_acyclic(e2, e1) }
+            catch {
+              case exn: Graph.Cycles[_] =>
+                error(cat_lines(exn.cycles.map(cycle =>
+                  "Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
+                  " due to session " + quote(s))))
+            }
+          }
+          else g3.add_edge(e2, e1)
         }
       }
     }
   }
 
+  val entries_graph: Graph[String, Unit] = dependency_graph(acyclic = false)
+
   def entries_graph_display: Graph_Display.Graph =
     Graph_Display.make_graph(entries_graph)
 

--- a/src/Pure/General/graph.ML	Tue Oct 10 17:15:37 2017 +0100
+++ b/src/Pure/General/graph.ML	Tue Oct 10 19:51:54 2017 +0200
@@ -40,6 +40,7 @@
   val maximals: 'a T -> key list
   val is_minimal: 'a T -> key -> bool
   val is_maximal: 'a T -> key -> bool
+  val is_isolated: 'a T -> key -> bool
   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
   val default_node: key * 'a -> 'a T -> 'a T
   val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
@@ -177,6 +178,8 @@
 fun is_minimal G x = Keys.is_empty (imm_preds G x);
 fun is_maximal G x = Keys.is_empty (imm_succs G x);
 
+fun is_isolated G x = is_minimal G x andalso is_maximal G x;
+
 
 (* node operations *)
 

--- a/src/Pure/General/graph.scala	Tue Oct 10 17:15:37 2017 +0100
+++ b/src/Pure/General/graph.scala	Tue Oct 10 19:51:54 2017 +0200
@@ -147,6 +147,8 @@
   def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
   def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
 
+  def is_isolated(x: Key): Boolean = is_minimal(x) && is_maximal(x)
+
 
   /* node operations */
 

--- a/src/Pure/Thy/sessions.scala	Tue Oct 10 17:15:37 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Oct 10 19:51:54 2017 +0200
@@ -267,8 +267,7 @@
               }
 
               val imports_subgraph =
-                sessions.imports_graph.restrict(
-                  sessions.imports_graph.all_preds(info.parent.toList ::: info.imports).toSet)
+                sessions.imports_graph.restrict(sessions.imports_graph.all_preds(info.deps).toSet)
 
               val graph0 =
                 (Graph_Display.empty_graph /: imports_subgraph.topological_order)(
@@ -356,7 +355,7 @@
   sealed case class Info(
     name: String,
     chapter: String,
-    select: Boolean,
+    dir_selected: Boolean,
     pos: Position.T,
     groups: List[String],
     dir: Path,
@@ -369,6 +368,8 @@
     document_files: List[(Path, Path)],
     meta_digest: SHA1.Digest)
   {
+    def deps: List[String] = parent.toList ::: imports
+
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
   }
 
@@ -424,7 +425,7 @@
           val select = sessions.toSet ++ graph.all_succs(base_sessions)
           (for {
             (name, (info, _)) <- graph.iterator
-            if info.select || select(name) || graph.get_node(name).groups.exists(select_group)
+            if info.dir_selected || select(name) || graph.get_node(name).groups.exists(select_group)
           } yield name).toList
         }
       }.filterNot(excluded)