# HG changeset patch # User wenzelm # Date 1342700680 -7200 # Node ID a78e5d3995993cca9dbff9cba1b2d2ef950aebb7 # Parent cbb25adad26ff9d6b976e1053fa98a738c19aac6 support Session.Queue with ordering and dependencies; diff -r cbb25adad26f -r a78e5d399599 src/FOL/ROOT --- a/src/FOL/ROOT Thu Jul 19 14:15:08 2012 +0200 +++ b/src/FOL/ROOT Thu Jul 19 14:24:40 2012 +0200 @@ -1,4 +1,4 @@ -session FOL! in "." = Pure + +session FOL! (10) in "." = Pure + description "First-Order Logic with Natural Deduction" options [proofs = 2] theories FOL diff -r cbb25adad26f -r a78e5d399599 src/HOL/ROOT --- a/src/HOL/ROOT Thu Jul 19 14:15:08 2012 +0200 +++ b/src/HOL/ROOT Thu Jul 19 14:24:40 2012 +0200 @@ -1,4 +1,4 @@ -session HOL! in "." = Pure + +session HOL! (1) in "." = Pure + description {* Classical Higher-order Logic *} options [document_graph] theories Complex_Main @@ -19,12 +19,12 @@ options [document = false] theories Main -session "HOL-Proofs"! in "." = Pure + +session "HOL-Proofs"! (2) in "." = Pure + description {* HOL-Main with proof terms *} options [document = false, proofs = 2, parallel_proofs = false] theories Main -session HOLCF! = HOL + +session HOLCF! (3) = HOL + description {* Author: Franz Regensburger Author: Brian Huffman diff -r cbb25adad26f -r a78e5d399599 src/Pure/Isar/parse.scala --- a/src/Pure/Isar/parse.scala Thu Jul 19 14:15:08 2012 +0200 +++ b/src/Pure/Isar/parse.scala Thu Jul 19 14:24:40 2012 +0200 @@ -54,6 +54,7 @@ tok => tok.kind == Token.Kind.KEYWORD && tok.content == name) def string: Parser[String] = atom("string", _.is_string) + def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s)) def name: Parser[String] = atom("name declaration", _.is_name) def xname: Parser[String] = atom("name reference", _.is_xname) def text: Parser[String] = atom("text", _.is_text) diff -r cbb25adad26f -r a78e5d399599 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Thu Jul 19 14:15:08 2012 +0200 +++ b/src/Pure/Isar/token.scala Thu Jul 19 14:24:40 2012 +0200 @@ -74,6 +74,7 @@ kind == Token.Kind.VERBATIM || kind == Token.Kind.COMMENT def is_string: Boolean = kind == Token.Kind.STRING + def is_nat: Boolean = kind == Token.Kind.NAT def is_name: Boolean = kind == Token.Kind.IDENT || kind == Token.Kind.SYM_IDENT || diff -r cbb25adad26f -r a78e5d399599 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Thu Jul 19 14:15:08 2012 +0200 +++ b/src/Pure/System/build.scala Thu Jul 19 14:24:40 2012 +0200 @@ -19,14 +19,73 @@ type Options = List[(String, Option[String])] - case class Session_Info( - dir: Path, - name: String, - parent: Option[String], - description: String, - options: Options, - theories: List[(Options, String)], - files: List[String]) + object Session + { + object Key + { + object Ordering extends scala.math.Ordering[Key] + { + def compare(key1: Key, key2: Key): Int = + key2.order compare key1.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 + } + + sealed case class Info( + dir: Path, + key: Key, + parent: Option[String], + description: String, + options: Options, + theories: List[(Options, String)], + files: List[String]) + { + def name: String = key.name + } + + object Queue + { + val empty: Queue = new Queue() + } + + final class Queue private( + keys: Map[String, Key] = Map.empty, + graph: Graph[Key, Info] = Graph.empty(Key.Ordering)) + { + def lookup(name: String): Option[Info] = + keys.get(name).map(graph.get_node(_)) + + def + (info: Info): Queue = + { + val keys1 = + if (keys.isDefinedAt(info.name)) error("Duplicate session: " + quote(info.name)) + else keys + (info.name -> info.key) + + val graph1 = + try { + graph.new_node(info.key, info). + add_deps_acyclic(info.key, info.parent.toList.map(keys(_))) + } + catch { + 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) + } + + def topological_order: List[Info] = + graph.topological_order.map(graph.get_node(_)) + } + } /* parsing */ @@ -36,6 +95,7 @@ private case class Session_Entry( name: String, reset: Boolean, + order: Int, path: Option[String], parent: Option[String], description: String, @@ -71,13 +131,14 @@ ((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 => Session_Entry(a, b, c, d, e, f, g, h) } + { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) } } def parse_entries(root: File): List[Session_Entry] = @@ -93,9 +154,9 @@ /* find sessions */ - def find_sessions(more_dirs: List[Path]): List[Session_Info] = + def find_sessions(more_dirs: List[Path]): Session.Queue = { - val infos = new mutable.ListBuffer[Session_Info] + var sessions = Session.Queue.empty for { (dir, strict) <- Isabelle_System.components().map((_, false)) ++ more_dirs.map((_, true)) @@ -118,8 +179,8 @@ case None => error("Missing parent session") case Some(parent) => val parent_info = - infos.find(_.name == parent) getOrElse - error("Undefined parent session: " + quote(parent)) + sessions.lookup(parent) getOrElse + error("Undefined parent session: " + quote(parent)) if (entry.reset) entry.name else parent_info.name + "-" + entry.name } @@ -131,12 +192,10 @@ } val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten val info = - Session_Info(dir + path, full_name, entry.parent, entry.description, - entry.options, thys, entry.files) + Session.Info(dir + path, Session.Key(full_name, entry.order), + entry.parent, entry.description, entry.options, thys, entry.files) - if (infos.exists(_.name == full_name)) - error("Duplicate session: " + quote(full_name)) - infos += info + sessions += info } catch { case ERROR(msg) => @@ -144,7 +203,7 @@ quote(entry.name) + " (file " + quote(root.toString) + ")") } } - infos.toList + sessions } @@ -158,7 +217,8 @@ println("options = " + options.toString) println("sessions = " + sessions.toString) - find_sessions(more_dirs) foreach println + for (info <- find_sessions(more_dirs).topological_order) + println(info.name + " in " + info.dir) 0 } diff -r cbb25adad26f -r a78e5d399599 src/ZF/ROOT --- a/src/ZF/ROOT Thu Jul 19 14:15:08 2012 +0200 +++ b/src/ZF/ROOT Thu Jul 19 14:24:40 2012 +0200 @@ -1,4 +1,4 @@ -session ZF! in "." = FOL + +session ZF! (10) in "." = FOL + description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge