# HG changeset patch # User wenzelm # Date 1491481976 -7200 # Node ID 2b819faf45e91f5427f84143ab7fbda921891815 # Parent 4a042bf9488e7458b6fde470a029d5ae3ac87fdf clarified modules; diff -r 4a042bf9488e -r 2b819faf45e9 src/Pure/Thy/present.scala --- 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") diff -r 4a042bf9488e -r 2b819faf45e9 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Apr 06 14:08:42 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Thu Apr 06 14:32:56 2017 +0200 @@ -140,8 +140,7 @@ keywords = keywords, syntax = syntax, sources = all_files.map(p => (p, SHA1.digest(p.file))), - session_graph = - Present.session_graph(info.parent getOrElse "", parent_base, thy_deps.deps)) + session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base)) deps + (name -> base) } diff -r 4a042bf9488e -r 2b819faf45e9 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Thu Apr 06 14:08:42 2017 +0200 +++ b/src/Pure/Thy/thy_info.scala Thu Apr 06 14:32:56 2017 +0200 @@ -100,6 +100,26 @@ ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files } } + def session_graph(parent_session: String, parent_base: Sessions.Base): 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)) + } + } + } + override def toString: String = deps.toString }