# HG changeset patch
# User wenzelm
# Date 1491481976 -7200
# Node ID 2b819faf45e91f5427f84143ab7fbda921891815
# Parent  4a042bf9488e7458b6fde470a029d5ae3ac87fdf
clarified modules;

diff -r 4a042bf9488e -r 2b819faf45e9 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Thu Apr 06 14:08:42 2017 +0200
+++ b/src/Pure/Thy/present.scala	Thu Apr 06 14:32:56 2017 +0200
@@ -14,32 +14,6 @@
 
 object Present
 {
-  /* session graph */
-
-  def session_graph(
-    parent_session: String,
-    parent_base: Sessions.Base,
-    deps: List[Thy_Info.Dep]): Graph_Display.Graph =
-  {
-    val parent_session_node =
-      Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
-
-    def node(name: Document.Node.Name): Graph_Display.Node =
-      if (parent_base.loaded_theory(name)) parent_session_node
-      else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory)
-
-    (Graph_Display.empty_graph /: deps) {
-      case (g, dep) =>
-        if (parent_base.loaded_theory(dep.name)) g
-        else {
-          val a = node(dep.name)
-          val bs = dep.header.imports.map({ case (name, _) => node(name) })
-          ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
-        }
-    }
-  }
-
-
   /* maintain chapter index -- NOT thread-safe */
 
   private val index_path = Path.basic("index.html")
diff -r 4a042bf9488e -r 2b819faf45e9 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Apr 06 14:08:42 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Apr 06 14:32:56 2017 +0200
@@ -140,8 +140,7 @@
                 keywords = keywords,
                 syntax = syntax,
                 sources = all_files.map(p => (p, SHA1.digest(p.file))),
-                session_graph =
-                  Present.session_graph(info.parent getOrElse "", parent_base, thy_deps.deps))
+                session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base))
 
             deps + (name -> base)
           }
diff -r 4a042bf9488e -r 2b819faf45e9 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Thu Apr 06 14:08:42 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Thu Apr 06 14:32:56 2017 +0200
@@ -100,6 +100,26 @@
       ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
     }
 
+    def session_graph(parent_session: String, parent_base: Sessions.Base): Graph_Display.Graph =
+    {
+      val parent_session_node =
+        Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
+
+      def node(name: Document.Node.Name): Graph_Display.Node =
+        if (parent_base.loaded_theory(name)) parent_session_node
+        else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory)
+
+      (Graph_Display.empty_graph /: deps) {
+        case (g, dep) =>
+          if (parent_base.loaded_theory(dep.name)) g
+          else {
+            val a = node(dep.name)
+            val bs = dep.header.imports.map({ case (name, _) => node(name) })
+            ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
+          }
+      }
+    }
+
     override def toString: String = deps.toString
   }