# HG changeset patch # User wenzelm # Date 1344109541 -7200 # Node ID 3ef82491cdd6b326f3a1e8a8ce851162987d7ed5 # Parent 10f5303f86e5ac32a98d6f266fa295c09749d77e clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering); diff -r 10f5303f86e5 -r 3ef82491cdd6 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Sat Aug 04 20:28:35 2012 +0200 +++ b/src/Pure/System/build.scala Sat Aug 04 21:45:41 2012 +0200 @@ -12,7 +12,7 @@ BufferedReader, InputStreamReader, IOException} import java.util.zip.GZIPInputStream -import scala.collection.mutable +import scala.collection.SortedSet import scala.annotation.tailrec @@ -92,6 +92,76 @@ } + /* session tree */ + + object Session_Tree + { + def apply(infos: Seq[(String, Session_Info)]): Session_Tree = + { + val graph = + (Graph.string[Option[Session_Info]] /: infos) { + case (graph, (name, info)) => + val parents = info.parent.toList + + val graph1 = (graph /: (name :: parents))(_.default_node(_, None)) + if (graph1.get_node(name).isDefined) + error("Duplicate session: " + quote(name) + Position.str_of(info.pos)) + + try { graph1.map_node(name, _ => Some(info)).add_deps_acyclic(name, parents) } + catch { + case exn: Graph.Cycles[_] => + error(cat_lines(exn.cycles.map(cycle => + "Cyclic session dependency of " + + cycle.map(c => quote(c.toString)).mkString(" via ")))) + } + } + val tree = new Session_Tree(graph) + + val bad_parents = + (for { + (name, (Some(info), _)) <- graph.entries + if info.parent.isDefined; parent = info.parent.get + if !tree.isDefinedAt(parent) + } yield parent + " (for " + name + ")").toList + if (!bad_parents.isEmpty) error("Bad parent session(s): " + commas(bad_parents)) + + tree + } + } + + final class Session_Tree private(val graph: Graph[String, Option[Session_Info]]) + extends PartialFunction[String, Session_Info] + { + def apply(name: String): Session_Info = graph.get_node(name).get + def isDefinedAt(name: String): Boolean = + graph.defined(name) && graph.get_node(name).isDefined + + def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String]) + : (List[String], Session_Tree) = + { + val bad_sessions = sessions.filterNot(isDefinedAt(_)) + if (!bad_sessions.isEmpty) error("Undefined session(s): " + commas_quote(bad_sessions)) + + val selected = + { + if (all_sessions) graph.keys.toList + else { + val sel_group = session_groups.toSet + val sel = sessions.toSet + graph.keys.toList.filter(name => + sel(name) || apply(name).groups.exists(sel_group)).toList + } + } + val descendants = graph.all_succs(selected) + val tree1 = new Session_Tree(graph.restrict(graph.all_preds(selected).toSet)) + (descendants, tree1) + } + + def topological_order: List[(String, Session_Info)] = + graph.topological_order.map(name => (name, apply(name))) + } + + /* parser */ private object Parser extends Parse.Parser @@ -155,97 +225,10 @@ else error("Bad session root file: " + root.toString) } - def find_sessions(options: Options, more_dirs: List[Path]): List[(String, Session_Info)] = + def find_sessions(options: Options, more_dirs: List[Path]): Session_Tree = { val dirs = Isabelle_System.components().filter(is_session_dir(_)) ::: more_dirs - dirs.map(sessions_root(options, _)).flatten - } - - - object Session - { - object Queue - { - val empty: Queue = new Queue() - def apply(args: Seq[(String, Session_Info)]): Queue = - (empty /: args) { case (queue, (name, info)) => queue + (name, info) } - } - - final class Queue private(graph: Graph[String, Option[Session_Info]] = Graph.string) - extends PartialFunction[String, Session_Info] - { - def apply(name: String): Session_Info = graph.get_node(name).get - def isDefinedAt(name: String): Boolean = - graph.defined(name) && graph.get_node(name).isDefined - - def is_inner(name: String): Boolean = !graph.is_maximal(name) - - def is_empty: Boolean = graph.is_empty - - def + (name: String, info: Session_Info): Queue = - { - val parents = info.parent.toList - - val graph1 = (graph /: (name :: parents))(_.default_node(_, None)) - if (graph1.get_node(name).isDefined) - error("Duplicate session: " + quote(name) + Position.str_of(info.pos)) - - new Queue( - try { graph1.map_node(name, _ => Some(info)).add_deps_acyclic(name, parents) } - catch { - case exn: Graph.Cycles[_] => - error(cat_lines(exn.cycles.map(cycle => - "Cyclic session dependency of " + - cycle.map(c => quote(c.toString)).mkString(" via ")))) - }) - } - - def - (name: String): Queue = new Queue(graph.del_node(name)) - - def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String]) - : (List[String], Queue) = - { - (for { - (name, (Some(info), _)) <- graph.entries - if info.parent.isDefined; parent = info.parent.get - if !isDefinedAt(parent) - } yield parent + " (for " + name + ")").toList match - { - case Nil => - case bad => error("Bad parent session(s): " + commas(bad)) - } - - sessions.filterNot(isDefinedAt(_)) match { - case Nil => - case bad => error("Undefined session(s): " + commas_quote(bad)) - } - - val selected = - { - if (all_sessions) graph.keys.toList - else { - val sel_group = session_groups.toSet - val sel = sessions.toSet - graph.keys.toList.filter(name => - sel(name) || apply(name).groups.exists(sel_group)).toList - } - } - val descendants = graph.all_succs(selected) - val queue1 = new Queue(graph.restrict(graph.all_preds(selected).toSet)) - (descendants, queue1) - } - - def dequeue(skip: String => Boolean): Option[(String, Session_Info)] = - { - val it = graph.entries.dropWhile( - { case (name, (info, (deps, _))) => !deps.isEmpty || info.isEmpty || skip(name) }) - if (it.hasNext) { val (name, (info, _)) = it.next; Some((name, info.get)) } - else None - } - - def topological_order: List[(String, Session_Info)] = - graph.topological_order.map(name => (name, apply(name))) - } + Session_Tree(dirs.map(sessions_root(options, _)).flatten) } @@ -256,6 +239,34 @@ private def sleep(): Unit = Thread.sleep(500) + /* queue */ + + object Queue + { + def apply(tree: Session_Tree): Queue = + { + val graph = tree.graph + new Queue(graph, SortedSet(graph.keys.toList: _*)(graph.ordering)) + } + } + + final class Queue private(graph: Graph[String, Option[Session_Info]], order: SortedSet[String]) + { + def is_inner(name: String): Boolean = !graph.is_maximal(name) + + def is_empty: Boolean = graph.is_empty + + def - (name: String): Queue = new Queue(graph.del_node(name), order - name) + + def dequeue(skip: String => Boolean): Option[(String, Session_Info)] = + { + val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name)) + if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name).get)) } + else None + } + } + + /* source dependencies */ sealed case class Node( @@ -270,8 +281,8 @@ def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2) } - def dependencies(verbose: Boolean, queue: Session.Queue): Deps = - Deps((Map.empty[String, Node] /: queue.topological_order)( + def dependencies(verbose: Boolean, tree: Session_Tree): Deps = + Deps((Map.empty[String, Node] /: tree.topological_order)( { case (deps, (name, info)) => val (preloaded, parent_syntax) = info.parent match { @@ -475,13 +486,13 @@ sessions: List[String] = Nil): Int = { val options = (Options.init() /: build_options)(_.define_simple(_)) - val (descendants, queue) = - Session.Queue(find_sessions(options, more_dirs)) - .required(all_sessions, session_groups, sessions) - val deps = dependencies(verbose, queue) + val (descendants, tree) = + find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions) + val deps = dependencies(verbose, tree) + val queue = Queue(tree) def make_stamp(name: String): String = - sources_stamp(queue(name).entry_digest :: deps.sources(name)) + sources_stamp(tree(name).entry_digest :: deps.sources(name)) val (input_dirs, output_dir, browser_info) = if (system_mode) { @@ -511,7 +522,7 @@ case class Result(current: Boolean, heap: String, rc: Int) @tailrec def loop( - pending: Session.Queue, + pending: Queue, running: Map[String, (String, Job)], results: Map[String, Result]): Map[String, Result] = { @@ -644,9 +655,8 @@ // FIXME Symbol.decode!? def outer_syntax(session: String): Outer_Syntax = { - val (_, queue) = - Session.Queue(find_sessions(Options.init(), Nil)).required(false, Nil, List(session)) - dependencies(false, queue)(session).syntax + val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session)) + dependencies(false, tree)(session).syntax } }