1.1 --- a/src/HOL/ROOT Thu Jul 26 11:46:30 2012 +0200
1.2 +++ b/src/HOL/ROOT Thu Jul 26 11:52:08 2012 +0200
1.3 @@ -1,4 +1,4 @@
1.4 -session HOL! (1) in "." = Pure +
1.5 +session HOL! in "." = Pure +
1.6 description {* Classical Higher-order Logic *}
1.7 options [document_graph]
1.8 theories Complex_Main
1.9 @@ -19,7 +19,7 @@
1.10 options [document = false]
1.11 theories Main
1.12
1.13 -session "HOL-Proofs"! (4) in "." = Pure +
1.14 +session "HOL-Proofs"! in "." = Pure +
1.15 description {* HOL-Main with proof terms *}
1.16 options [document = false, proofs = 2, parallel_proofs = 0]
1.17 theories Main
1.18 @@ -571,7 +571,7 @@
1.19 "ex/Koepf_Duermuth_Countermeasure"
1.20 files "document/root.tex"
1.21
1.22 -session Nominal (2) = HOL +
1.23 +session Nominal = HOL +
1.24 options [document = false]
1.25 theories Nominal
1.26
1.27 @@ -760,7 +760,7 @@
1.28 Predicate_Compile_Tests
1.29 Specialisation_Examples
1.30
1.31 -session HOLCF! (3) = HOL +
1.32 +session HOLCF! = HOL +
1.33 description {*
1.34 Author: Franz Regensburger
1.35 Author: Brian Huffman
2.1 --- a/src/Pure/System/build.scala Thu Jul 26 11:46:30 2012 +0200
2.2 +++ b/src/Pure/System/build.scala Thu Jul 26 11:52:08 2012 +0200
2.3 @@ -21,26 +21,6 @@
2.4
2.5 object Session
2.6 {
2.7 - /* Key */
2.8 -
2.9 - object Key
2.10 - {
2.11 - object Ordering extends scala.math.Ordering[Key]
2.12 - {
2.13 - def compare(key1: Key, key2: Key): Int =
2.14 - key1.order compare key2.order match {
2.15 - case 0 => key1.name compare key2.name
2.16 - case ord => ord
2.17 - }
2.18 - }
2.19 - }
2.20 -
2.21 - sealed case class Key(name: String, order: Int)
2.22 - {
2.23 - override def toString: String = name
2.24 - }
2.25 -
2.26 -
2.27 /* Info */
2.28
2.29 sealed case class Info(
2.30 @@ -62,55 +42,42 @@
2.31 val empty: Queue = new Queue()
2.32 }
2.33
2.34 - final class Queue private(
2.35 - keys: Map[String, Key] = Map.empty,
2.36 - graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
2.37 + final class Queue private(graph: Graph[String, Info] = Graph.string)
2.38 + extends PartialFunction[String, Info]
2.39 {
2.40 + def apply(name: String): Info = graph.get_node(name)
2.41 + def isDefinedAt(name: String): Boolean = graph.defined(name)
2.42 +
2.43 + def is_inner(name: String): Boolean = !graph.is_maximal(name)
2.44 +
2.45 def is_empty: Boolean = graph.is_empty
2.46
2.47 - def apply(name: String): Info = graph.get_node(keys(name))
2.48 - def defined(name: String): Boolean = keys.isDefinedAt(name)
2.49 - def is_inner(name: String): Boolean = !graph.is_maximal(keys(name))
2.50 -
2.51 - def + (key: Key, info: Info): Queue =
2.52 - {
2.53 - val keys1 =
2.54 - if (defined(key.name)) error("Duplicate session: " + quote(key.name))
2.55 - else keys + (key.name -> key)
2.56 -
2.57 - val graph1 =
2.58 - try {
2.59 - graph.new_node(key, info).add_deps_acyclic(key, info.parent.toList.map(keys(_)))
2.60 - }
2.61 + def + (name: String, info: Info): Queue =
2.62 + new Queue(
2.63 + try { graph.new_node(name, info).add_deps_acyclic(name, info.parent.toList) }
2.64 catch {
2.65 + case _: Graph.Duplicate[_] => error("Duplicate session: " + quote(name))
2.66 case exn: Graph.Cycles[_] =>
2.67 error(cat_lines(exn.cycles.map(cycle =>
2.68 "Cyclic session dependency of " +
2.69 - cycle.map(key => quote(key.toString)).mkString(" via "))))
2.70 - }
2.71 - new Queue(keys1, graph1)
2.72 - }
2.73 + cycle.map(c => quote(c.toString)).mkString(" via "))))
2.74 + })
2.75
2.76 - def - (name: String): Queue = new Queue(keys - name, graph.del_node(keys(name)))
2.77 + def - (name: String): Queue = new Queue(graph.del_node(name))
2.78
2.79 def required(names: List[String]): Queue =
2.80 - {
2.81 - val req = graph.all_preds(names.map(keys(_))).map(_.name).toSet
2.82 - val keys1 = keys -- keys.keySet.filter(name => !req(name))
2.83 - val graph1 = graph.restrict(key => keys1.isDefinedAt(key.name))
2.84 - new Queue(keys1, graph1)
2.85 - }
2.86 + new Queue(graph.restrict(graph.all_preds(names).toSet))
2.87
2.88 def dequeue(skip: String => Boolean): Option[(String, Info)] =
2.89 {
2.90 val it = graph.entries.dropWhile(
2.91 - { case (key, (_, (deps, _))) => !deps.isEmpty || skip(key.name) })
2.92 - if (it.hasNext) { val (key, (info, _)) = it.next; Some((key.name, info)) }
2.93 + { case (name, (_, (deps, _))) => !deps.isEmpty || skip(name) })
2.94 + if (it.hasNext) { val (name, (info, _)) = it.next; Some((name, info)) }
2.95 else None
2.96 }
2.97
2.98 def topological_order: List[(String, Info)] =
2.99 - graph.topological_order.map(key => (key.name, graph.get_node(key)))
2.100 + graph.topological_order.map(name => (name, graph.get_node(name)))
2.101 }
2.102 }
2.103
2.104 @@ -120,7 +87,6 @@
2.105 private case class Session_Entry(
2.106 name: String,
2.107 this_name: Boolean,
2.108 - order: Int,
2.109 path: Option[String],
2.110 parent: Option[String],
2.111 description: String,
2.112 @@ -155,14 +121,13 @@
2.113
2.114 ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
2.115 (keyword("!") ^^^ true | success(false)) ~
2.116 - (keyword("(") ~! (nat <~ keyword(")")) ^^ { case _ ~ x => x } | success(Integer.MAX_VALUE)) ~
2.117 (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
2.118 (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
2.119 (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
2.120 (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
2.121 rep(theories) ~
2.122 (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
2.123 - { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
2.124 + { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) }
2.125 }
2.126
2.127 def parse_entries(root: JFile): List[Session_Entry] =
2.128 @@ -197,7 +162,7 @@
2.129 }
2.130 else
2.131 entry.parent match {
2.132 - case Some(parent_name) if queue1.defined(parent_name) =>
2.133 + case Some(parent_name) if queue1.isDefinedAt(parent_name) =>
2.134 val full_name =
2.135 if (entry.this_name) entry.name
2.136 else parent_name + "-" + entry.name
2.137 @@ -212,8 +177,6 @@
2.138 case None => Path.basic(entry.name)
2.139 }
2.140
2.141 - val key = Session.Key(full_name, entry.order)
2.142 -
2.143 val session_options = options ++ entry.options
2.144
2.145 val theories =
2.146 @@ -226,7 +189,7 @@
2.147 Session.Info(entry.name, dir + path, entry.parent, parent_base_name,
2.148 entry.description, session_options, theories, files, digest)
2.149
2.150 - queue1 + (key, info)
2.151 + queue1 + (full_name, info)
2.152 }
2.153 catch {
2.154 case ERROR(msg) =>
2.155 @@ -276,7 +239,7 @@
2.156
2.157 for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
2.158
2.159 - sessions.filter(name => !queue.defined(name)) match {
2.160 + sessions.filter(name => !queue.isDefinedAt(name)) match {
2.161 case Nil =>
2.162 case bad => error("Undefined session(s): " + commas_quote(bad))
2.163 }