1.1 --- a/src/Pure/System/build.scala Sat Jul 21 21:16:08 2012 +0200
1.2 +++ b/src/Pure/System/build.scala Sat Jul 21 22:13:50 2012 +0200
1.3 @@ -17,10 +17,10 @@
1.4 {
1.5 /** session information **/
1.6
1.7 - type Options = List[(String, Option[String])]
1.8 -
1.9 object Session
1.10 {
1.11 + /* Key */
1.12 +
1.13 object Key
1.14 {
1.15 object Ordering extends scala.math.Ordering[Key]
1.16 @@ -38,13 +38,24 @@
1.17 override def toString: String = name
1.18 }
1.19
1.20 +
1.21 + /* Info */
1.22 +
1.23 + sealed abstract class Status
1.24 + case object Pending extends Status
1.25 + case object Running extends Status
1.26 +
1.27 sealed case class Info(
1.28 dir: Path,
1.29 parent: Option[String],
1.30 description: String,
1.31 options: Options,
1.32 - theories: List[(Options, List[String])],
1.33 - files: List[String])
1.34 + theories: List[(Options, List[Path])],
1.35 + files: List[Path],
1.36 + status: Status = Pending)
1.37 +
1.38 +
1.39 + /* Queue */
1.40
1.41 object Queue
1.42 {
1.43 @@ -101,8 +112,8 @@
1.44 path: Option[String],
1.45 parent: Option[String],
1.46 description: String,
1.47 - options: Options,
1.48 - theories: List[(Options, List[String])],
1.49 + options: List[Options.Spec],
1.50 + theories: List[(List[Options.Spec], List[String])],
1.51 files: List[String])
1.52
1.53 private object Parser extends Parse.Parser
1.54 @@ -161,7 +172,8 @@
1.55
1.56 private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
1.57
1.58 - private def sessions_root(dir: Path, root: JFile, queue: Session.Queue): Session.Queue =
1.59 + private def sessions_root(options: Options, dir: Path, root: JFile, queue: Session.Queue)
1.60 + : Session.Queue =
1.61 {
1.62 (queue /: Parser.parse_entries(root))((queue1, entry) =>
1.63 try {
1.64 @@ -187,9 +199,13 @@
1.65 }
1.66
1.67 val key = Session.Key(full_name, entry.order)
1.68 +
1.69 + val theories =
1.70 + entry.theories.map({ case (opts, thys) => (options ++ opts, thys.map(Path.explode(_))) })
1.71 + val files = entry.files.map(Path.explode(_))
1.72 val info =
1.73 Session.Info(dir + path, entry.parent,
1.74 - entry.description, entry.options, entry.theories, entry.files)
1.75 + entry.description, options ++ entry.options, theories, files)
1.76
1.77 queue1 + (key, info)
1.78 }
1.79 @@ -200,22 +216,24 @@
1.80 })
1.81 }
1.82
1.83 - private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue =
1.84 + private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue)
1.85 + : Session.Queue =
1.86 {
1.87 val root = (dir + ROOT).file
1.88 - if (root.isFile) sessions_root(dir, root, queue)
1.89 + if (root.isFile) sessions_root(options, dir, root, queue)
1.90 else if (strict) error("Bad session root file: " + quote(root.toString))
1.91 else queue
1.92 }
1.93
1.94 - private def sessions_catalog(dir: Path, catalog: JFile, queue: Session.Queue): Session.Queue =
1.95 + private def sessions_catalog(options: Options, dir: Path, catalog: JFile, queue: Session.Queue)
1.96 + : Session.Queue =
1.97 {
1.98 val dirs =
1.99 split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
1.100 (queue /: dirs)((queue1, dir1) =>
1.101 try {
1.102 val dir2 = dir + Path.explode(dir1)
1.103 - if (dir2.file.isDirectory) sessions_dir(true, dir2, queue1)
1.104 + if (dir2.file.isDirectory) sessions_dir(options, true, dir2, queue1)
1.105 else error("Bad session directory: " + dir2.toString)
1.106 }
1.107 catch {
1.108 @@ -224,20 +242,20 @@
1.109 })
1.110 }
1.111
1.112 - def find_sessions(all_sessions: Boolean, sessions: List[String],
1.113 + def find_sessions(options: Options, all_sessions: Boolean, sessions: List[String],
1.114 more_dirs: List[Path]): Session.Queue =
1.115 {
1.116 var queue = Session.Queue.empty
1.117
1.118 for (dir <- Isabelle_System.components()) {
1.119 - queue = sessions_dir(false, dir, queue)
1.120 + queue = sessions_dir(options, false, dir, queue)
1.121
1.122 val catalog = (dir + SESSIONS).file
1.123 if (catalog.isFile)
1.124 - queue = sessions_catalog(dir, catalog, queue)
1.125 + queue = sessions_catalog(options, dir, catalog, queue)
1.126 }
1.127
1.128 - for (dir <- more_dirs) queue = sessions_dir(true, dir, queue)
1.129 + for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
1.130
1.131 sessions.filter(name => !queue.defined(name)) match {
1.132 case Nil =>
1.133 @@ -300,9 +318,8 @@
1.134 val args_xml =
1.135 {
1.136 import XML.Encode._
1.137 - def symbol_string: T[String] = (s => string(Symbol.encode(s)))
1.138 - pair(bool, pair(symbol_string, pair(symbol_string, list(symbol_string))))(
1.139 - save, (parent, (name, info.theories.map(_._2).flatten)))
1.140 + pair(bool, pair(string, pair(string, list(string))))(
1.141 + save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
1.142 }
1.143 new Build_Job(cwd, env, script, YXML.string_of_body(args_xml))
1.144 }
1.145 @@ -311,7 +328,7 @@
1.146 more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
1.147 {
1.148 val options = (Options.init() /: more_options)(_.define_simple(_))
1.149 - val queue = find_sessions(all_sessions, sessions, more_dirs)
1.150 + val queue = find_sessions(options, all_sessions, sessions, more_dirs)
1.151
1.152
1.153 // prepare browser info dir