--- 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")