src/Pure/Thy/sessions.scala
changeset 65507 decdb95bd007
parent 65500 a6644e0e8728
child 65517 1544e61e5314
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Apr 18 19:14:01 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Apr 18 19:17:46 2017 +0200
     1.3 @@ -204,6 +204,39 @@
     1.4              if (check_keywords.nonEmpty)
     1.5                Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
     1.6  
     1.7 +            val session_graph: Graph_Display.Graph =
     1.8 +            {
     1.9 +              def session_node(name: String): Graph_Display.Node =
    1.10 +                Graph_Display.Node("[" + name + "]", "session." + name)
    1.11 +
    1.12 +              def node(name: Document.Node.Name): Graph_Display.Node =
    1.13 +              {
    1.14 +                val session = resources.theory_qualifier(name)
    1.15 +                if (session == session_name)
    1.16 +                  Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
    1.17 +                else session_node(session)
    1.18 +              }
    1.19 +
    1.20 +              val imports_subgraph =
    1.21 +                sessions.imports_graph.restrict(
    1.22 +                  sessions.imports_graph.all_preds(info.parent.toList ::: info.imports).toSet)
    1.23 +
    1.24 +              val graph0 =
    1.25 +                (Graph_Display.empty_graph /: imports_subgraph.topological_order)(
    1.26 +                  { case (g, session) =>
    1.27 +                      val a = session_node(session)
    1.28 +                      val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_))
    1.29 +                      ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
    1.30 +
    1.31 +              (graph0 /: thy_deps.deps)(
    1.32 +                { case (g, dep) =>
    1.33 +                    val a = node(dep.name)
    1.34 +                    val bs =
    1.35 +                      dep.header.imports.map({ case (name, _) => node(name) }).
    1.36 +                        filterNot(_ == a)
    1.37 +                    ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
    1.38 +            }
    1.39 +
    1.40              val base =
    1.41                Base(global_theories = global_theories,
    1.42                  loaded_theories = thy_deps.loaded_theories,
    1.43 @@ -211,7 +244,7 @@
    1.44                  keywords = thy_deps.keywords,
    1.45                  syntax = syntax,
    1.46                  sources = all_files.map(p => (p, SHA1.digest(p.file))),
    1.47 -                session_graph = thy_deps.session_graph(info.parent getOrElse "", imports_base))
    1.48 +                session_graph = session_graph)
    1.49  
    1.50              session_bases + (session_name -> base)
    1.51            }