# HG changeset patch # User wenzelm # Date 1491558649 -7200 # Node ID 695d4e22345a9f6e2c25994f3eece12d38aef95a # Parent 457e4fbed73179cdabdd71bac01a3c796ef172d7 support for static session imports, without affect build hierarchy; diff -r 457e4fbed731 -r 695d4e22345a src/Pure/Admin/build_doc.scala --- a/src/Pure/Admin/build_doc.scala Fri Apr 07 10:47:25 2017 +0200 +++ b/src/Pure/Admin/build_doc.scala Fri Apr 07 11:50:49 2017 +0200 @@ -24,7 +24,7 @@ { val selection = for { - (name, info) <- Sessions.load(options).topological_order + (name, info) <- Sessions.load(options).build_topological_order if info.groups.contains("doc") doc = info.options.string("document_variants") if all_docs || docs.contains(doc) diff -r 457e4fbed731 -r 695d4e22345a src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Apr 07 10:47:25 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Fri Apr 07 11:50:49 2017 +0200 @@ -57,7 +57,7 @@ check_keywords: Set[String] = Set.empty, global_theories: Set[String] = Set.empty): Deps = { - Deps((Map.empty[String, Base] /: sessions.topological_order)({ + Deps((Map.empty[String, Base] /: sessions.imports_topological_order)({ case (sessions, (name, info)) => if (progress.stopped) throw Exn.Interrupt() @@ -173,6 +173,7 @@ parent: Option[String], description: String, options: Options, + imports: List[String], theories: List[(Options, List[String])], global_theories: List[String], files: List[Path], @@ -235,7 +236,29 @@ def make(infos: Traversable[(String, Info)]): T = { - val graph1 = + def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String]) + : Graph[String, Info] = + { + def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) = + { + if (!g.defined(parent)) + error("Bad " + kind + " session " + quote(parent) + " for " + + quote(name) + Position.here(pos)) + + try { g.add_edge_acyclic(parent, name) } + catch { + case exn: Graph.Cycles[_] => + error(cat_lines(exn.cycles.map(cycle => + "Cyclic session dependency of " + + cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos)) + } + } + (graph /: graph.iterator) { + case (g, (name, (info, _))) => (g /: edges(info))(add_edge(info.pos, name, _, _)) + } + } + + val graph0 = (Graph.string[Info] /: infos) { case (graph, (name, info)) => if (graph.defined(name)) @@ -243,55 +266,47 @@ Position.here(graph.get_node(name).pos)) else graph.new_node(name, info) } - val graph2 = - (graph1 /: graph1.iterator) { - case (graph, (name, (info, _))) => - info.parent match { - case None => graph - case Some(parent) => - if (!graph.defined(parent)) - error("Bad parent session " + quote(parent) + " for " + - quote(name) + Position.here(info.pos)) + val graph1 = add_edges(graph0, "parent", _.parent) + val graph2 = add_edges(graph1, "imports", _.imports) - try { graph.add_edge_acyclic(parent, name) } - catch { - case exn: Graph.Cycles[_] => - error(cat_lines(exn.cycles.map(cycle => - "Cyclic session dependency of " + - cycle.map(c => quote(c.toString)).mkString(" via "))) + - Position.here(info.pos)) - } - } - } - - new T(graph2) + new T(graph1, graph2) } - final class T private[Sessions](val graph: Graph[String, Info]) - extends PartialFunction[String, Info] + final class T private[Sessions]( + val build_graph: Graph[String, Info], + val imports_graph: Graph[String, Info]) { - def apply(name: String): Info = graph.get_node(name) - def isDefinedAt(name: String): Boolean = graph.defined(name) + def apply(name: String): Info = imports_graph.get_node(name) + def get(name: String): Option[Info] = + if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None def global_theories: Set[String] = (for { - (_, (info, _)) <- graph.iterator + (_, (info, _)) <- imports_graph.iterator name <- info.global_theories.iterator } yield name).toSet def selection(select: Selection): (List[String], T) = { - val (selected, graph1) = select(graph) - (selected, new T(graph1)) + val (_, build_graph1) = select(build_graph) + val (selected, imports_graph1) = select(imports_graph) + (selected, new T(build_graph1, imports_graph1)) } - def ancestors(name: String): List[String] = - graph.all_preds(List(name)).tail.reverse + def build_ancestors(name: String): List[String] = + build_graph.all_preds(List(name)).tail.reverse + + def build_descendants(names: List[String]): List[String] = + build_graph.all_succs(names) - def topological_order: List[(String, Info)] = - graph.topological_order.map(name => (name, apply(name))) + def build_topological_order: List[(String, Info)] = + build_graph.topological_order.map(name => (name, apply(name))) - override def toString: String = graph.keys_iterator.mkString("Sessions.T(", ", ", ")") + def imports_topological_order: List[(String, Info)] = + imports_graph.topological_order.map(name => (name, apply(name))) + + override def toString: String = + imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")") } @@ -305,6 +320,7 @@ private val IN = "in" private val DESCRIPTION = "description" private val OPTIONS = "options" + private val SESSIONS = "sessions" private val THEORIES = "theories" private val GLOBAL = "global" private val FILES = "files" @@ -316,6 +332,7 @@ (SESSION, Keyword.THY_DECL) + (DESCRIPTION, Keyword.QUASI_COMMAND) + (OPTIONS, Keyword.QUASI_COMMAND) + + (SESSIONS, Keyword.QUASI_COMMAND) + (THEORIES, Keyword.QUASI_COMMAND) + (FILES, Keyword.QUASI_COMMAND) + (DOCUMENT_FILES, Keyword.QUASI_COMMAND) @@ -332,6 +349,7 @@ parent: Option[String], description: String, options: List[Options.Spec], + imports: List[String], theories: List[(List[Options.Spec], List[(String, Boolean)])], files: List[String], document_files: List[(String, String)]) extends Entry @@ -377,11 +395,12 @@ (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~ (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~ (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~ + (($$$(SESSIONS) ~! rep(session_name) ^^ { case _ ~ x => x }) | success(Nil)) ~ rep1(theories) ~ (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~ (rep(document_files) ^^ (x => x.flatten))))) ^^ - { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) => - Session_Entry(pos, a, b, c, d, e, f, g, h, i) } + { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j))) => + Session_Entry(pos, a, b, c, d, e, f, g, h, i, j) } } def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] = @@ -415,12 +434,12 @@ val meta_digest = SHA1.digest((entry_chapter, name, entry.parent, entry.options, - entry.theories, entry.files, entry.document_files).toString) + entry.imports, entry.theories, entry.files, entry.document_files).toString) val info = Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path), - entry.parent, entry.description, session_options, theories, global_theories, - files, document_files, meta_digest) + entry.parent, entry.description, session_options, entry.imports, theories, + global_theories, files, document_files, meta_digest) (name, info) } diff -r 457e4fbed731 -r 695d4e22345a src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Apr 07 10:47:25 2017 +0200 +++ b/src/Pure/Tools/build.scala Fri Apr 07 11:50:49 2017 +0200 @@ -65,7 +65,7 @@ def apply(sessions: Sessions.T, store: Sessions.Store): Queue = { - val graph = sessions.graph + val graph = sessions.build_graph val names = graph.keys val timings = names.map(name => (name, load_timings(store, name))) @@ -413,7 +413,7 @@ // optional cleanup if (clean_build) { - for (name <- full_sessions.graph.all_succs(selected)) { + for (name <- full_sessions.build_descendants(selected)) { val files = List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)). map(store.output_dir + _).filter(_.is_file) @@ -519,7 +519,7 @@ //{{{ check/start next job pending.dequeue(running.isDefinedAt(_)) match { case Some((name, info)) => - val ancestor_results = selected_sessions.ancestors(name).map(results(_)) + val ancestor_results = selected_sessions.build_ancestors(name).map(results(_)) val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp) val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name) diff -r 457e4fbed731 -r 695d4e22345a src/Pure/Tools/ml_process.scala --- a/src/Pure/Tools/ml_process.scala Fri Apr 07 10:47:25 2017 +0200 +++ b/src/Pure/Tools/ml_process.scala Fri Apr 07 11:50:49 2017 +0200 @@ -33,7 +33,7 @@ val selection = Sessions.Selection(sessions = List(logic_name)) val (_, selected_sessions) = sessions.getOrElse(Sessions.load(options, dirs)).selection(selection) - (selected_sessions.ancestors(logic_name) ::: List(logic_name)). + (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)). map(a => File.platform_path(store.heap(a))) } diff -r 457e4fbed731 -r 695d4e22345a src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Apr 07 10:47:25 2017 +0200 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Apr 07 11:50:49 2017 +0200 @@ -41,7 +41,7 @@ tree <- try { Some(Sessions.load(session_options(options), dirs = session_dirs())) } catch { case ERROR(_) => None } - info <- tree.lift(logic) + info <- tree.get(logic) parent <- info.parent if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true" } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none) @@ -77,7 +77,7 @@ { val session_tree = Sessions.load(options, dirs = session_dirs()) val (main_sessions, other_sessions) = - session_tree.topological_order.partition(p => p._2.groups.contains("main")) + session_tree.imports_topological_order.partition(p => p._2.groups.contains("main")) main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted }