src/Pure/Thy/present.scala
changeset 60077 55cb9462e602
parent 51987 7d8e0e3c553b
child 61372 cf40b6b1de54
     1.1 --- a/src/Pure/Thy/present.scala	Wed Apr 15 14:54:25 2015 +0200
     1.2 +++ b/src/Pure/Thy/present.scala	Wed Apr 15 15:27:45 2015 +0200
     1.3 @@ -12,6 +12,32 @@
     1.4  
     1.5  object Present
     1.6  {
     1.7 +  /* session graph */
     1.8 +
     1.9 +  def session_graph(
    1.10 +    parent_session: String,
    1.11 +    parent_loaded: String => Boolean,
    1.12 +    deps: List[Thy_Info.Dep]): Graph_Display.Graph =
    1.13 +  {
    1.14 +    val parent_session_node =
    1.15 +      Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
    1.16 +
    1.17 +    def node(name: Document.Node.Name): Graph_Display.Node =
    1.18 +      if (parent_loaded(name.theory)) parent_session_node
    1.19 +      else Graph_Display.Node(name.theory, "theory." + name.theory)
    1.20 +
    1.21 +    (Graph_Display.empty_graph /: deps) {
    1.22 +      case (g, dep) =>
    1.23 +        if (parent_loaded(dep.name.theory)) g
    1.24 +        else {
    1.25 +          val a = node(dep.name)
    1.26 +          val bs = dep.header.imports.map({ case (name, _) => node(name) })
    1.27 +          ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
    1.28 +        }
    1.29 +    }
    1.30 +  }
    1.31 +
    1.32 +
    1.33    /* maintain chapter index -- NOT thread-safe */
    1.34  
    1.35    private val index_path = Path.basic("index.html")
    1.36 @@ -48,4 +74,3 @@
    1.37      File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
    1.38    }
    1.39  }
    1.40 -