support for session graph from Scala side;
authorwenzelm
Sun Jan 25 20:22:20 2015 +0100 (2015-01-25)
changeset 59444d57e275b2d82
parent 59443 5b552b4f63a5
child 59445 2c27c3d1fd3b
support for session graph from Scala side;
src/Pure/Thy/thy_info.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/thy_info.scala	Sun Jan 25 20:16:27 2015 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.scala	Sun Jan 25 20:22:20 2015 +0100
     1.3 @@ -91,6 +91,26 @@
     1.4            rev_deps)
     1.5        ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
     1.6      }
     1.7 +
     1.8 +    def deps_graph(parent_session: String, parent_loaded: String => Boolean): Graph_Display.Graph =
     1.9 +    {
    1.10 +      val parent_session_node =
    1.11 +        Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
    1.12 +
    1.13 +      def node(name: Document.Node.Name): Graph_Display.Node =
    1.14 +        if (parent_loaded(name.theory)) parent_session_node
    1.15 +        else Graph_Display.Node(name.theory, "theory." + name.theory)
    1.16 +
    1.17 +      (Graph_Display.empty_graph /: rev_deps) {
    1.18 +        case (g, dep) =>
    1.19 +          if (parent_loaded(dep.name.theory)) g
    1.20 +          else {
    1.21 +            val a = node(dep.name)
    1.22 +            val bs = dep.header.imports.map(node _)
    1.23 +            ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
    1.24 +          }
    1.25 +      }
    1.26 +    }
    1.27    }
    1.28  
    1.29    private def require_thys(session: String, initiators: List[Document.Node.Name],
     2.1 --- a/src/Pure/Tools/build.scala	Sun Jan 25 20:16:27 2015 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Sun Jan 25 20:22:20 2015 +0100
     2.3 @@ -416,7 +416,8 @@
     2.4      known_theories: Map[String, Document.Node.Name],
     2.5      keywords: Thy_Header.Keywords,
     2.6      syntax: Outer_Syntax,
     2.7 -    sources: List[(Path, SHA1.Digest)])
     2.8 +    sources: List[(Path, SHA1.Digest)],
     2.9 +    session_graph: Graph_Display.Graph)
    2.10  
    2.11    sealed case class Deps(deps: Map[String, Session_Content])
    2.12    {
    2.13 @@ -494,8 +495,11 @@
    2.14  
    2.15              val sources = all_files.map(p => (p, SHA1.digest(p.file)))
    2.16  
    2.17 +            val session_graph = thy_deps.deps_graph(info.parent getOrElse "", loaded_theories0)
    2.18 +
    2.19              val content =
    2.20 -              Session_Content(loaded_theories, known_theories, keywords, syntax, sources)
    2.21 +              Session_Content(loaded_theories, known_theories, keywords, syntax,
    2.22 +                sources, session_graph)
    2.23              deps + (name -> content)
    2.24            }
    2.25            catch {