clarified session graph: collapse theories from other sessions;
authorwenzelm
Tue Apr 18 19:17:46 2017 +0200 (2017-04-18)
changeset 65507decdb95bd007
parent 65506 359fc6266a00
child 65508 a72ab197e681
clarified session graph: collapse theories from other sessions;
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.scala
     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            }
     2.1 --- a/src/Pure/Thy/thy_info.scala	Tue Apr 18 19:14:01 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Apr 18 19:17:46 2017 +0200
     2.3 @@ -101,26 +101,6 @@
     2.4        ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
     2.5      }
     2.6  
     2.7 -    def session_graph(parent_session: String, parent_base: Sessions.Base): Graph_Display.Graph =
     2.8 -    {
     2.9 -      val parent_session_node =
    2.10 -        Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
    2.11 -
    2.12 -      def node(name: Document.Node.Name): Graph_Display.Node =
    2.13 -        if (parent_base.loaded_theory(name)) parent_session_node
    2.14 -        else Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
    2.15 -
    2.16 -      (Graph_Display.empty_graph /: deps) {
    2.17 -        case (g, dep) =>
    2.18 -          if (parent_base.loaded_theory(dep.name)) g
    2.19 -          else {
    2.20 -            val a = node(dep.name)
    2.21 -            val bs = dep.header.imports.map({ case (name, _) => node(name) })
    2.22 -            ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
    2.23 -          }
    2.24 -      }
    2.25 -    }
    2.26 -
    2.27      override def toString: String = deps.toString
    2.28    }
    2.29