# HG changeset patch # User wenzelm # Date 1343296328 -7200 # Node ID 5a59e4c0395762b4693cd519469db3b166944514 # Parent 1182677e472821b6ed39e738c3e3374222099bf3 discontinued slightly odd session order, which did not quite work out; diff -r 1182677e4728 -r 5a59e4c03957 src/HOL/ROOT --- a/src/HOL/ROOT Thu Jul 26 11:46:30 2012 +0200 +++ b/src/HOL/ROOT Thu Jul 26 11:52:08 2012 +0200 @@ -1,4 +1,4 @@ -session HOL! (1) in "." = Pure + +session HOL! in "." = Pure + description {* Classical Higher-order Logic *} options [document_graph] theories Complex_Main @@ -19,7 +19,7 @@ options [document = false] theories Main -session "HOL-Proofs"! (4) in "." = Pure + +session "HOL-Proofs"! in "." = Pure + description {* HOL-Main with proof terms *} options [document = false, proofs = 2, parallel_proofs = 0] theories Main @@ -571,7 +571,7 @@ "ex/Koepf_Duermuth_Countermeasure" files "document/root.tex" -session Nominal (2) = HOL + +session Nominal = HOL + options [document = false] theories Nominal @@ -760,7 +760,7 @@ Predicate_Compile_Tests Specialisation_Examples -session HOLCF! (3) = HOL + +session HOLCF! = HOL + description {* Author: Franz Regensburger Author: Brian Huffman diff -r 1182677e4728 -r 5a59e4c03957 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Thu Jul 26 11:46:30 2012 +0200 +++ b/src/Pure/System/build.scala Thu Jul 26 11:52:08 2012 +0200 @@ -21,26 +21,6 @@ object Session { - /* Key */ - - object Key - { - object Ordering extends scala.math.Ordering[Key] - { - def compare(key1: Key, key2: Key): Int = - key1.order compare key2.order match { - case 0 => key1.name compare key2.name - case ord => ord - } - } - } - - sealed case class Key(name: String, order: Int) - { - override def toString: String = name - } - - /* Info */ sealed case class Info( @@ -62,55 +42,42 @@ val empty: Queue = new Queue() } - final class Queue private( - keys: Map[String, Key] = Map.empty, - graph: Graph[Key, Info] = Graph.empty(Key.Ordering)) + final class Queue private(graph: Graph[String, Info] = Graph.string) + extends PartialFunction[String, Info] { + def apply(name: String): Info = graph.get_node(name) + def isDefinedAt(name: String): Boolean = graph.defined(name) + + def is_inner(name: String): Boolean = !graph.is_maximal(name) + def is_empty: Boolean = graph.is_empty - def apply(name: String): Info = graph.get_node(keys(name)) - def defined(name: String): Boolean = keys.isDefinedAt(name) - def is_inner(name: String): Boolean = !graph.is_maximal(keys(name)) - - def + (key: Key, info: Info): Queue = - { - val keys1 = - if (defined(key.name)) error("Duplicate session: " + quote(key.name)) - else keys + (key.name -> key) - - val graph1 = - try { - graph.new_node(key, info).add_deps_acyclic(key, info.parent.toList.map(keys(_))) - } + def + (name: String, info: Info): Queue = + new Queue( + try { graph.new_node(name, info).add_deps_acyclic(name, info.parent.toList) } catch { + case _: Graph.Duplicate[_] => error("Duplicate session: " + quote(name)) case exn: Graph.Cycles[_] => error(cat_lines(exn.cycles.map(cycle => "Cyclic session dependency of " + - cycle.map(key => quote(key.toString)).mkString(" via ")))) - } - new Queue(keys1, graph1) - } + cycle.map(c => quote(c.toString)).mkString(" via ")))) + }) - def - (name: String): Queue = new Queue(keys - name, graph.del_node(keys(name))) + def - (name: String): Queue = new Queue(graph.del_node(name)) def required(names: List[String]): Queue = - { - val req = graph.all_preds(names.map(keys(_))).map(_.name).toSet - val keys1 = keys -- keys.keySet.filter(name => !req(name)) - val graph1 = graph.restrict(key => keys1.isDefinedAt(key.name)) - new Queue(keys1, graph1) - } + new Queue(graph.restrict(graph.all_preds(names).toSet)) def dequeue(skip: String => Boolean): Option[(String, Info)] = { val it = graph.entries.dropWhile( - { case (key, (_, (deps, _))) => !deps.isEmpty || skip(key.name) }) - if (it.hasNext) { val (key, (info, _)) = it.next; Some((key.name, info)) } + { case (name, (_, (deps, _))) => !deps.isEmpty || skip(name) }) + if (it.hasNext) { val (name, (info, _)) = it.next; Some((name, info)) } else None } def topological_order: List[(String, Info)] = - graph.topological_order.map(key => (key.name, graph.get_node(key))) + graph.topological_order.map(name => (name, graph.get_node(name))) } } @@ -120,7 +87,6 @@ private case class Session_Entry( name: String, this_name: Boolean, - order: Int, path: Option[String], parent: Option[String], description: String, @@ -155,14 +121,13 @@ ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~ (keyword("!") ^^^ true | success(false)) ~ - (keyword("(") ~! (nat <~ keyword(")")) ^^ { case _ ~ x => x } | success(Integer.MAX_VALUE)) ~ (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~ (keyword("=") ~> opt(session_name <~ keyword("+"))) ~ (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~ (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~ rep(theories) ~ (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^ - { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) } + { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) } } def parse_entries(root: JFile): List[Session_Entry] = @@ -197,7 +162,7 @@ } else entry.parent match { - case Some(parent_name) if queue1.defined(parent_name) => + case Some(parent_name) if queue1.isDefinedAt(parent_name) => val full_name = if (entry.this_name) entry.name else parent_name + "-" + entry.name @@ -212,8 +177,6 @@ case None => Path.basic(entry.name) } - val key = Session.Key(full_name, entry.order) - val session_options = options ++ entry.options val theories = @@ -226,7 +189,7 @@ Session.Info(entry.name, dir + path, entry.parent, parent_base_name, entry.description, session_options, theories, files, digest) - queue1 + (key, info) + queue1 + (full_name, info) } catch { case ERROR(msg) => @@ -276,7 +239,7 @@ for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue) - sessions.filter(name => !queue.defined(name)) match { + sessions.filter(name => !queue.isDefinedAt(name)) match { case Nil => case bad => error("Undefined session(s): " + commas_quote(bad)) }