1.1 --- a/src/HOL/ROOT Sat Jul 21 21:16:08 2012 +0200
1.2 +++ b/src/HOL/ROOT Sat Jul 21 22:13:50 2012 +0200
1.3 @@ -21,7 +21,7 @@
1.4
1.5 session "HOL-Proofs"! (2) in "." = Pure +
1.6 description {* HOL-Main with proof terms *}
1.7 - options [document = false, proofs = 2, parallel_proofs = false]
1.8 + options [document = false, proofs = 2, parallel_proofs = 0]
1.9 theories Main
1.10
1.11 session HOLCF! (3) = HOL +
2.1 --- a/src/Pure/System/build.scala Sat Jul 21 21:16:08 2012 +0200
2.2 +++ b/src/Pure/System/build.scala Sat Jul 21 22:13:50 2012 +0200
2.3 @@ -17,10 +17,10 @@
2.4 {
2.5 /** session information **/
2.6
2.7 - type Options = List[(String, Option[String])]
2.8 -
2.9 object Session
2.10 {
2.11 + /* Key */
2.12 +
2.13 object Key
2.14 {
2.15 object Ordering extends scala.math.Ordering[Key]
2.16 @@ -38,13 +38,24 @@
2.17 override def toString: String = name
2.18 }
2.19
2.20 +
2.21 + /* Info */
2.22 +
2.23 + sealed abstract class Status
2.24 + case object Pending extends Status
2.25 + case object Running extends Status
2.26 +
2.27 sealed case class Info(
2.28 dir: Path,
2.29 parent: Option[String],
2.30 description: String,
2.31 options: Options,
2.32 - theories: List[(Options, List[String])],
2.33 - files: List[String])
2.34 + theories: List[(Options, List[Path])],
2.35 + files: List[Path],
2.36 + status: Status = Pending)
2.37 +
2.38 +
2.39 + /* Queue */
2.40
2.41 object Queue
2.42 {
2.43 @@ -101,8 +112,8 @@
2.44 path: Option[String],
2.45 parent: Option[String],
2.46 description: String,
2.47 - options: Options,
2.48 - theories: List[(Options, List[String])],
2.49 + options: List[Options.Spec],
2.50 + theories: List[(List[Options.Spec], List[String])],
2.51 files: List[String])
2.52
2.53 private object Parser extends Parse.Parser
2.54 @@ -161,7 +172,8 @@
2.55
2.56 private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
2.57
2.58 - private def sessions_root(dir: Path, root: JFile, queue: Session.Queue): Session.Queue =
2.59 + private def sessions_root(options: Options, dir: Path, root: JFile, queue: Session.Queue)
2.60 + : Session.Queue =
2.61 {
2.62 (queue /: Parser.parse_entries(root))((queue1, entry) =>
2.63 try {
2.64 @@ -187,9 +199,13 @@
2.65 }
2.66
2.67 val key = Session.Key(full_name, entry.order)
2.68 +
2.69 + val theories =
2.70 + entry.theories.map({ case (opts, thys) => (options ++ opts, thys.map(Path.explode(_))) })
2.71 + val files = entry.files.map(Path.explode(_))
2.72 val info =
2.73 Session.Info(dir + path, entry.parent,
2.74 - entry.description, entry.options, entry.theories, entry.files)
2.75 + entry.description, options ++ entry.options, theories, files)
2.76
2.77 queue1 + (key, info)
2.78 }
2.79 @@ -200,22 +216,24 @@
2.80 })
2.81 }
2.82
2.83 - private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue =
2.84 + private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue)
2.85 + : Session.Queue =
2.86 {
2.87 val root = (dir + ROOT).file
2.88 - if (root.isFile) sessions_root(dir, root, queue)
2.89 + if (root.isFile) sessions_root(options, dir, root, queue)
2.90 else if (strict) error("Bad session root file: " + quote(root.toString))
2.91 else queue
2.92 }
2.93
2.94 - private def sessions_catalog(dir: Path, catalog: JFile, queue: Session.Queue): Session.Queue =
2.95 + private def sessions_catalog(options: Options, dir: Path, catalog: JFile, queue: Session.Queue)
2.96 + : Session.Queue =
2.97 {
2.98 val dirs =
2.99 split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
2.100 (queue /: dirs)((queue1, dir1) =>
2.101 try {
2.102 val dir2 = dir + Path.explode(dir1)
2.103 - if (dir2.file.isDirectory) sessions_dir(true, dir2, queue1)
2.104 + if (dir2.file.isDirectory) sessions_dir(options, true, dir2, queue1)
2.105 else error("Bad session directory: " + dir2.toString)
2.106 }
2.107 catch {
2.108 @@ -224,20 +242,20 @@
2.109 })
2.110 }
2.111
2.112 - def find_sessions(all_sessions: Boolean, sessions: List[String],
2.113 + def find_sessions(options: Options, all_sessions: Boolean, sessions: List[String],
2.114 more_dirs: List[Path]): Session.Queue =
2.115 {
2.116 var queue = Session.Queue.empty
2.117
2.118 for (dir <- Isabelle_System.components()) {
2.119 - queue = sessions_dir(false, dir, queue)
2.120 + queue = sessions_dir(options, false, dir, queue)
2.121
2.122 val catalog = (dir + SESSIONS).file
2.123 if (catalog.isFile)
2.124 - queue = sessions_catalog(dir, catalog, queue)
2.125 + queue = sessions_catalog(options, dir, catalog, queue)
2.126 }
2.127
2.128 - for (dir <- more_dirs) queue = sessions_dir(true, dir, queue)
2.129 + for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
2.130
2.131 sessions.filter(name => !queue.defined(name)) match {
2.132 case Nil =>
2.133 @@ -300,9 +318,8 @@
2.134 val args_xml =
2.135 {
2.136 import XML.Encode._
2.137 - def symbol_string: T[String] = (s => string(Symbol.encode(s)))
2.138 - pair(bool, pair(symbol_string, pair(symbol_string, list(symbol_string))))(
2.139 - save, (parent, (name, info.theories.map(_._2).flatten)))
2.140 + pair(bool, pair(string, pair(string, list(string))))(
2.141 + save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
2.142 }
2.143 new Build_Job(cwd, env, script, YXML.string_of_body(args_xml))
2.144 }
2.145 @@ -311,7 +328,7 @@
2.146 more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
2.147 {
2.148 val options = (Options.init() /: more_options)(_.define_simple(_))
2.149 - val queue = find_sessions(all_sessions, sessions, more_dirs)
2.150 + val queue = find_sessions(options, all_sessions, sessions, more_dirs)
2.151
2.152
2.153 // prepare browser info dir
3.1 --- a/src/Pure/System/options.scala Sat Jul 21 21:16:08 2012 +0200
3.2 +++ b/src/Pure/System/options.scala Sat Jul 21 22:13:50 2012 +0200
3.3 @@ -12,19 +12,24 @@
3.4
3.5 object Options
3.6 {
3.7 - abstract class Type
3.8 + type Spec = (String, Option[String])
3.9 +
3.10 + val empty: Options = new Options()
3.11 +
3.12 +
3.13 + /* representation */
3.14 +
3.15 + sealed abstract class Type
3.16 {
3.17 def print: String = toString.toLowerCase
3.18 }
3.19 - case object Bool extends Type
3.20 - case object Int extends Type
3.21 - case object Real extends Type
3.22 - case object String extends Type
3.23 + private case object Bool extends Type
3.24 + private case object Int extends Type
3.25 + private case object Real extends Type
3.26 + private case object String extends Type
3.27
3.28 case class Opt(typ: Type, value: String, description: String)
3.29
3.30 - val empty: Options = new Options()
3.31 -
3.32
3.33 /* parsing */
3.34
3.35 @@ -58,7 +63,7 @@
3.36 }
3.37 }
3.38
3.39 - val OPTIONS = Path.explode("etc/options")
3.40 + private val OPTIONS = Path.explode("etc/options")
3.41
3.42 def init(): Options =
3.43 {
3.44 @@ -194,6 +199,9 @@
3.45 }
3.46 }
3.47
3.48 + def ++ (specs: List[Options.Spec]): Options =
3.49 + (this /: specs)({ case (x, (y, z)) => x.define(y, z) })
3.50 +
3.51 def define_simple(str: String): Options =
3.52 {
3.53 str.indexOf('=') match {