# HG changeset patch
# User wenzelm
# Date 1429117717 -7200
# Node ID d3573eb7728f8f40bfe2beba62c22f04ba97d0fe
# Parent  9fb7b44e3e7e4df93b61e245cbdcbe1f0939e16f
session graph with folded base theories, as in document preparation;

diff -r 9fb7b44e3e7e -r d3573eb7728f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Apr 15 17:34:45 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Apr 15 19:08:37 2015 +0200
@@ -270,33 +270,22 @@
 
 (* display dependencies *)
 
-val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  let
-    val thy = Toplevel.theory_of state;
-    val thy_session = Present.session_name thy;
-  in
-    Theory.nodes_of thy
-    |> map (fn thy_node =>
-        let
-          val name = Context.theory_name thy_node;
-          val parents = map Context.theory_name (Theory.parents_of thy_node);
-          val session = Present.session_name thy_node;
-          val node =
-            Graph_Display.session_node
-              {name = name, directory = session, unfold = session = thy_session, path = ""};
-        in ((name, node), parents) end)
-    |> Graph_Display.display_graph
-  end);
+val thy_deps =
+  Toplevel.unknown_theory o
+  Toplevel.keep (fn st =>
+    let
+      val thy = Toplevel.theory_of st;
+      val parent_session = Session.get_name ();
+      val parent_loaded = is_some o Thy_Info.lookup_theory;
+    in Graph_Display.display_graph (Present.session_graph parent_session parent_loaded thy) end);
 
-val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  let
-    val thy = Toplevel.theory_of state;
-  in
+val locale_deps =
+  Toplevel.unknown_theory o
+  Toplevel.keep (Toplevel.theory_of #> (fn thy =>
     Locale.pretty_locale_deps thy
     |> map (fn {name, parents, body} =>
       ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
-    |> Graph_Display.display_graph
-  end);
+    |> Graph_Display.display_graph));
 
 
 (* print theorems, terms, types etc. *)
diff -r 9fb7b44e3e7e -r d3573eb7728f src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Apr 15 17:34:45 2015 +0200
+++ b/src/Pure/Thy/present.ML	Wed Apr 15 19:08:37 2015 +0200
@@ -7,6 +7,7 @@
 signature PRESENT =
 sig
   val session_name: theory -> string
+  val session_graph: string -> (string -> bool) -> theory -> Graph_Display.entry list
   val document_enabled: string -> bool
   val document_variants: string -> (string * string) list
   val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
@@ -54,6 +55,28 @@
 val session_name = #name o Browser_Info.get;
 
 
+(* session graph *)
+
+fun session_graph parent_session parent_loaded =
+  let
+    val parent_session_name = "session." ^ parent_session;
+    val parent_session_node = Graph_Display.content_node ("[" ^ parent_session ^ "]") [];
+    fun node_name name = if parent_loaded name then parent_session_name else "theory." ^ name;
+    fun theory_entry thy =
+      let
+        val name = Context.theory_name thy;
+        val deps = map (node_name o Context.theory_name) (Theory.parents_of thy);
+      in
+        if parent_loaded name then NONE
+        else SOME ((node_name name, Graph_Display.content_node name []), deps)
+      end;
+  in
+    fn thy =>
+      ((parent_session_name, parent_session_node), []) ::
+        map_filter theory_entry (Theory.nodes_of thy)
+  end;
+
+
 
 (** global browser info state **)
 
@@ -366,4 +389,3 @@
   end);
 
 end;
-