# HG changeset patch # User wenzelm # Date 1342901630 -7200 # Node ID c4d337782de4b2bca615b20c0f3f3ca161338f85 # Parent a8ed41b6280bb31e8c444983d217595f2b31a907 propagate defined options; misc tuning; diff -r a8ed41b6280b -r c4d337782de4 src/HOL/ROOT --- a/src/HOL/ROOT Sat Jul 21 21:16:08 2012 +0200 +++ b/src/HOL/ROOT Sat Jul 21 22:13:50 2012 +0200 @@ -21,7 +21,7 @@ session "HOL-Proofs"! (2) in "." = Pure + description {* HOL-Main with proof terms *} - options [document = false, proofs = 2, parallel_proofs = false] + options [document = false, proofs = 2, parallel_proofs = 0] theories Main session HOLCF! (3) = HOL + diff -r a8ed41b6280b -r c4d337782de4 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Sat Jul 21 21:16:08 2012 +0200 +++ b/src/Pure/System/build.scala Sat Jul 21 22:13:50 2012 +0200 @@ -17,10 +17,10 @@ { /** session information **/ - type Options = List[(String, Option[String])] - object Session { + /* Key */ + object Key { object Ordering extends scala.math.Ordering[Key] @@ -38,13 +38,24 @@ override def toString: String = name } + + /* Info */ + + sealed abstract class Status + case object Pending extends Status + case object Running extends Status + sealed case class Info( dir: Path, parent: Option[String], description: String, options: Options, - theories: List[(Options, List[String])], - files: List[String]) + theories: List[(Options, List[Path])], + files: List[Path], + status: Status = Pending) + + + /* Queue */ object Queue { @@ -101,8 +112,8 @@ path: Option[String], parent: Option[String], description: String, - options: Options, - theories: List[(Options, List[String])], + options: List[Options.Spec], + theories: List[(List[Options.Spec], List[String])], files: List[String]) private object Parser extends Parse.Parser @@ -161,7 +172,8 @@ private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure" - private def sessions_root(dir: Path, root: JFile, queue: Session.Queue): Session.Queue = + private def sessions_root(options: Options, dir: Path, root: JFile, queue: Session.Queue) + : Session.Queue = { (queue /: Parser.parse_entries(root))((queue1, entry) => try { @@ -187,9 +199,13 @@ } val key = Session.Key(full_name, entry.order) + + val theories = + entry.theories.map({ case (opts, thys) => (options ++ opts, thys.map(Path.explode(_))) }) + val files = entry.files.map(Path.explode(_)) val info = Session.Info(dir + path, entry.parent, - entry.description, entry.options, entry.theories, entry.files) + entry.description, options ++ entry.options, theories, files) queue1 + (key, info) } @@ -200,22 +216,24 @@ }) } - private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue = + private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue) + : Session.Queue = { val root = (dir + ROOT).file - if (root.isFile) sessions_root(dir, root, queue) + if (root.isFile) sessions_root(options, dir, root, queue) else if (strict) error("Bad session root file: " + quote(root.toString)) else queue } - private def sessions_catalog(dir: Path, catalog: JFile, queue: Session.Queue): Session.Queue = + private def sessions_catalog(options: Options, dir: Path, catalog: JFile, queue: Session.Queue) + : Session.Queue = { val dirs = split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#")) (queue /: dirs)((queue1, dir1) => try { val dir2 = dir + Path.explode(dir1) - if (dir2.file.isDirectory) sessions_dir(true, dir2, queue1) + if (dir2.file.isDirectory) sessions_dir(options, true, dir2, queue1) else error("Bad session directory: " + dir2.toString) } catch { @@ -224,20 +242,20 @@ }) } - def find_sessions(all_sessions: Boolean, sessions: List[String], + def find_sessions(options: Options, all_sessions: Boolean, sessions: List[String], more_dirs: List[Path]): Session.Queue = { var queue = Session.Queue.empty for (dir <- Isabelle_System.components()) { - queue = sessions_dir(false, dir, queue) + queue = sessions_dir(options, false, dir, queue) val catalog = (dir + SESSIONS).file if (catalog.isFile) - queue = sessions_catalog(dir, catalog, queue) + queue = sessions_catalog(options, dir, catalog, queue) } - for (dir <- more_dirs) queue = sessions_dir(true, dir, queue) + for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue) sessions.filter(name => !queue.defined(name)) match { case Nil => @@ -300,9 +318,8 @@ val args_xml = { import XML.Encode._ - def symbol_string: T[String] = (s => string(Symbol.encode(s))) - pair(bool, pair(symbol_string, pair(symbol_string, list(symbol_string))))( - save, (parent, (name, info.theories.map(_._2).flatten))) + pair(bool, pair(string, pair(string, list(string))))( + save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode)))) } new Build_Job(cwd, env, script, YXML.string_of_body(args_xml)) } @@ -311,7 +328,7 @@ more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int = { val options = (Options.init() /: more_options)(_.define_simple(_)) - val queue = find_sessions(all_sessions, sessions, more_dirs) + val queue = find_sessions(options, all_sessions, sessions, more_dirs) // prepare browser info dir diff -r a8ed41b6280b -r c4d337782de4 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sat Jul 21 21:16:08 2012 +0200 +++ b/src/Pure/System/options.scala Sat Jul 21 22:13:50 2012 +0200 @@ -12,19 +12,24 @@ object Options { - abstract class Type + type Spec = (String, Option[String]) + + val empty: Options = new Options() + + + /* representation */ + + sealed abstract class Type { def print: String = toString.toLowerCase } - case object Bool extends Type - case object Int extends Type - case object Real extends Type - case object String extends Type + private case object Bool extends Type + private case object Int extends Type + private case object Real extends Type + private case object String extends Type case class Opt(typ: Type, value: String, description: String) - val empty: Options = new Options() - /* parsing */ @@ -58,7 +63,7 @@ } } - val OPTIONS = Path.explode("etc/options") + private val OPTIONS = Path.explode("etc/options") def init(): Options = { @@ -194,6 +199,9 @@ } } + def ++ (specs: List[Options.Spec]): Options = + (this /: specs)({ case (x, (y, z)) => x.define(y, z) }) + def define_simple(str: String): Options = { str.indexOf('=') match {