diff -r 719f458cd89e -r 5b51ccdc8623 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Tue Aug 07 16:34:15 2012 +0200 +++ b/src/Pure/System/build.scala Tue Aug 07 17:08:22 2012 +0200 @@ -315,22 +315,22 @@ } - /* source dependencies */ + /* source dependencies and static content */ - sealed case class Node( + sealed case class Session_Content( loaded_theories: Set[String], syntax: Outer_Syntax, sources: List[(Path, SHA1.Digest)]) - sealed case class Deps(deps: Map[String, Node]) + sealed case class Deps(deps: Map[String, Session_Content]) { def is_empty: Boolean = deps.isEmpty - def apply(name: String): Node = deps(name) + def apply(name: String): Session_Content = deps(name) def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2) } def dependencies(verbose: Boolean, tree: Session_Tree): Deps = - Deps((Map.empty[String, Node] /: tree.topological_order)( + Deps((Map.empty[String, Session_Content] /: tree.topological_order)( { case (deps, (name, info)) => val (preloaded, parent_syntax) = info.parent match { @@ -374,9 +374,17 @@ quote(name) + Position.str_of(info.pos)) } - deps + (name -> Node(loaded_theories, syntax, sources)) + deps + (name -> Session_Content(loaded_theories, syntax, sources)) })) + def session_content(session: String): Session_Content = + { + val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session)) + dependencies(false, tree)(session) + } + + def outer_syntax(session: String): Outer_Syntax = session_content(session).syntax + /* jobs */ @@ -391,7 +399,7 @@ browser_info + Path.explode("isabelle.gif")) File.write(browser_info + Path.explode("index.html"), File.read(Path.explode("~~/lib/html/library_index_header.template")) + - File.read(Path.explode("~~/lib/html/library_index_content.template")) + + File.read(Path.explode("~~/lib/html/library_index_Session_Content.template")) + File.read(Path.explode("~~/lib/html/library_index_footer.template"))) } @@ -695,14 +703,5 @@ } } } - - - /* static outer syntax */ - - def outer_syntax(session: String): Outer_Syntax = - { - val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session)) - dependencies(false, tree)(session).syntax - } }