--- 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
--- 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
--- 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)
--- 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 ||
--- 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
}
--- 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