--- 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;
-