1.1 --- a/lib/Tools/build Sun Jul 22 10:00:51 2012 +0200
1.2 +++ b/lib/Tools/build Sun Jul 22 23:36:11 2012 +0200
1.3 @@ -18,8 +18,10 @@
1.4 echo " -a all sessions"
1.5 echo " -b build target images"
1.6 echo " -d DIR additional session directory with ROOT file"
1.7 + echo " -j INT maximum number of jobs (default 1)"
1.8 echo " -l list sessions only"
1.9 echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)"
1.10 + echo " -v verbose"
1.11 echo
1.12 echo " Build and manage Isabelle sessions, depending on implicit"
1.13 echo " ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
1.14 @@ -38,17 +40,24 @@
1.15 exit 2
1.16 }
1.17
1.18 +function check_number()
1.19 +{
1.20 + [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
1.21 +}
1.22 +
1.23
1.24 ## process command line
1.25
1.26 ALL_SESSIONS=false
1.27 BUILD_IMAGES=false
1.28 +MAX_JOBS=1
1.29 LIST_ONLY=false
1.30 +VERBOSE=false
1.31
1.32 declare -a MORE_DIRS=()
1.33 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
1.34
1.35 -while getopts "abd:lo:" OPT
1.36 +while getopts "abd:j:lo:v" OPT
1.37 do
1.38 case "$OPT" in
1.39 a)
1.40 @@ -60,12 +69,19 @@
1.41 d)
1.42 MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
1.43 ;;
1.44 + j)
1.45 + check_number "$OPTARG"
1.46 + MAX_JOBS="$OPTARG"
1.47 + ;;
1.48 l)
1.49 LIST_ONLY="true"
1.50 ;;
1.51 o)
1.52 BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
1.53 ;;
1.54 + v)
1.55 + VERBOSE="true"
1.56 + ;;
1.57 \?)
1.58 usage
1.59 ;;
1.60 @@ -80,5 +96,5 @@
1.61 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
1.62
1.63 exec "$ISABELLE_TOOL" java isabelle.Build \
1.64 - "$ALL_SESSIONS" "$BUILD_IMAGES" "$LIST_ONLY" \
1.65 + "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$VERBOSE" \
1.66 "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
2.1 --- a/src/HOL/ROOT Sun Jul 22 10:00:51 2012 +0200
2.2 +++ b/src/HOL/ROOT Sun Jul 22 23:36:11 2012 +0200
2.3 @@ -21,7 +21,7 @@
2.4
2.5 session "HOL-Proofs"! (2) in "." = Pure +
2.6 description {* HOL-Main with proof terms *}
2.7 - options [document = false, proofs = 2, parallel_proofs = false]
2.8 + options [document = false, proofs = 2, parallel_proofs = 0]
2.9 theories Main
2.10
2.11 session HOLCF! (3) = HOL +
3.1 --- a/src/Pure/General/path.ML Sun Jul 22 10:00:51 2012 +0200
3.2 +++ b/src/Pure/General/path.ML Sun Jul 22 23:36:11 2012 +0200
3.3 @@ -51,7 +51,7 @@
3.4 | check_elem (chs as ["~"]) = err_elem "Illegal" chs
3.5 | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
3.6 | check_elem chs =
3.7 - (case inter (op =) ["/", "\\", ":"] chs of
3.8 + (case inter (op =) ["/", "\\", "$", ":", "\"", "'"] chs of
3.9 [] => chs
3.10 | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
3.11
4.1 --- a/src/Pure/General/path.scala Sun Jul 22 10:00:51 2012 +0200
4.2 +++ b/src/Pure/General/path.scala Sun Jul 22 23:36:11 2012 +0200
4.3 @@ -29,7 +29,8 @@
4.4 private def check_elem(s: String): String =
4.5 if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
4.6 else
4.7 - s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
4.8 + s.iterator.filter(c =>
4.9 + c == '/' || c == '\\' || c == '$' || c == ':' || c == '"' || c == '\'').toList match {
4.10 case Nil => s
4.11 case bads =>
4.12 err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s)
5.1 --- a/src/Pure/General/sha1.scala Sun Jul 22 10:00:51 2012 +0200
5.2 +++ b/src/Pure/General/sha1.scala Sun Jul 22 23:36:11 2012 +0200
5.3 @@ -48,6 +48,8 @@
5.4 make_result(digest)
5.5 }
5.6
5.7 + def digest(path: Path): Digest = digest(path.file)
5.8 +
5.9 def digest(bytes: Array[Byte]): Digest =
5.10 {
5.11 val digest = MessageDigest.getInstance("SHA")
6.1 --- a/src/Pure/ROOT Sun Jul 22 10:00:51 2012 +0200
6.2 +++ b/src/Pure/ROOT Sun Jul 22 23:36:11 2012 +0200
6.3 @@ -20,5 +20,6 @@
6.4 "ML-Systems/use_context.ML"
6.5
6.6 session Pure in "." =
6.7 + theories Pure
6.8 files "ROOT.ML" (* FIXME *)
6.9
7.1 --- a/src/Pure/System/build.scala Sun Jul 22 10:00:51 2012 +0200
7.2 +++ b/src/Pure/System/build.scala Sun Jul 22 23:36:11 2012 +0200
7.3 @@ -17,10 +17,10 @@
7.4 {
7.5 /** session information **/
7.6
7.7 - type Options = List[(String, Option[String])]
7.8 -
7.9 object Session
7.10 {
7.11 + /* Key */
7.12 +
7.13 object Key
7.14 {
7.15 object Ordering extends scala.math.Ordering[Key]
7.16 @@ -38,13 +38,20 @@
7.17 override def toString: String = name
7.18 }
7.19
7.20 +
7.21 + /* Info */
7.22 +
7.23 sealed case class Info(
7.24 dir: Path,
7.25 parent: Option[String],
7.26 description: String,
7.27 options: Options,
7.28 - theories: List[(Options, List[String])],
7.29 - files: List[String])
7.30 + theories: List[(Options, List[Path])],
7.31 + files: List[Path],
7.32 + digest: SHA1.Digest)
7.33 +
7.34 +
7.35 + /* Queue */
7.36
7.37 object Queue
7.38 {
7.39 @@ -55,8 +62,10 @@
7.40 keys: Map[String, Key] = Map.empty,
7.41 graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
7.42 {
7.43 + def is_empty: Boolean = graph.is_empty
7.44 +
7.45 + def apply(name: String): Info = graph.get_node(keys(name))
7.46 def defined(name: String): Boolean = keys.isDefinedAt(name)
7.47 -
7.48 def is_inner(name: String): Boolean = !graph.is_maximal(keys(name))
7.49
7.50 def + (key: Key, info: Info): Queue =
7.51 @@ -78,6 +87,8 @@
7.52 new Queue(keys1, graph1)
7.53 }
7.54
7.55 + def - (name: String): Queue = new Queue(keys - name, graph.del_node(keys(name)))
7.56 +
7.57 def required(names: List[String]): Queue =
7.58 {
7.59 val req = graph.all_preds(names.map(keys(_))).map(_.name).toSet
7.60 @@ -86,8 +97,16 @@
7.61 new Queue(keys1, graph1)
7.62 }
7.63
7.64 - def topological_order: List[(Key, Info)] =
7.65 - graph.topological_order.map(key => (key, graph.get_node(key)))
7.66 + def dequeue(skip: String => Boolean): Option[(String, Info)] =
7.67 + {
7.68 + val it = graph.entries.dropWhile(
7.69 + { case (key, (_, (deps, _))) => !deps.isEmpty || skip(key.name) })
7.70 + if (it.hasNext) { val (key, (info, _)) = it.next; Some((key.name, info)) }
7.71 + else None
7.72 + }
7.73 +
7.74 + def topological_order: List[(String, Info)] =
7.75 + graph.topological_order.map(key => (key.name, graph.get_node(key)))
7.76 }
7.77 }
7.78
7.79 @@ -101,8 +120,8 @@
7.80 path: Option[String],
7.81 parent: Option[String],
7.82 description: String,
7.83 - options: Options,
7.84 - theories: List[(Options, List[String])],
7.85 + options: List[Options.Spec],
7.86 + theories: List[(List[Options.Spec], List[String])],
7.87 files: List[String])
7.88
7.89 private object Parser extends Parse.Parser
7.90 @@ -161,7 +180,8 @@
7.91
7.92 private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
7.93
7.94 - private def sessions_root(dir: Path, root: JFile, queue: Session.Queue): Session.Queue =
7.95 + private def sessions_root(options: Options, dir: Path, root: JFile, queue: Session.Queue)
7.96 + : Session.Queue =
7.97 {
7.98 (queue /: Parser.parse_entries(root))((queue1, entry) =>
7.99 try {
7.100 @@ -187,9 +207,15 @@
7.101 }
7.102
7.103 val key = Session.Key(full_name, entry.order)
7.104 +
7.105 + val theories =
7.106 + entry.theories.map({ case (opts, thys) => (options ++ opts, thys.map(Path.explode(_))) })
7.107 + val files = entry.files.map(Path.explode(_))
7.108 + val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
7.109 +
7.110 val info =
7.111 Session.Info(dir + path, entry.parent,
7.112 - entry.description, entry.options, entry.theories, entry.files)
7.113 + entry.description, options ++ entry.options, theories, files, digest)
7.114
7.115 queue1 + (key, info)
7.116 }
7.117 @@ -200,22 +226,24 @@
7.118 })
7.119 }
7.120
7.121 - private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue =
7.122 + private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue)
7.123 + : Session.Queue =
7.124 {
7.125 val root = (dir + ROOT).file
7.126 - if (root.isFile) sessions_root(dir, root, queue)
7.127 + if (root.isFile) sessions_root(options, dir, root, queue)
7.128 else if (strict) error("Bad session root file: " + quote(root.toString))
7.129 else queue
7.130 }
7.131
7.132 - private def sessions_catalog(dir: Path, catalog: JFile, queue: Session.Queue): Session.Queue =
7.133 + private def sessions_catalog(options: Options, dir: Path, catalog: JFile, queue: Session.Queue)
7.134 + : Session.Queue =
7.135 {
7.136 val dirs =
7.137 split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
7.138 (queue /: dirs)((queue1, dir1) =>
7.139 try {
7.140 val dir2 = dir + Path.explode(dir1)
7.141 - if (dir2.file.isDirectory) sessions_dir(true, dir2, queue1)
7.142 + if (dir2.file.isDirectory) sessions_dir(options, true, dir2, queue1)
7.143 else error("Bad session directory: " + dir2.toString)
7.144 }
7.145 catch {
7.146 @@ -224,20 +252,20 @@
7.147 })
7.148 }
7.149
7.150 - def find_sessions(all_sessions: Boolean, sessions: List[String],
7.151 + def find_sessions(options: Options, all_sessions: Boolean, sessions: List[String],
7.152 more_dirs: List[Path]): Session.Queue =
7.153 {
7.154 var queue = Session.Queue.empty
7.155
7.156 for (dir <- Isabelle_System.components()) {
7.157 - queue = sessions_dir(false, dir, queue)
7.158 + queue = sessions_dir(options, false, dir, queue)
7.159
7.160 val catalog = (dir + SESSIONS).file
7.161 if (catalog.isFile)
7.162 - queue = sessions_catalog(dir, catalog, queue)
7.163 + queue = sessions_catalog(options, dir, catalog, queue)
7.164 }
7.165
7.166 - for (dir <- more_dirs) queue = sessions_dir(true, dir, queue)
7.167 + for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
7.168
7.169 sessions.filter(name => !queue.defined(name)) match {
7.170 case Nil =>
7.171 @@ -251,25 +279,68 @@
7.172
7.173 /** build **/
7.174
7.175 - private def echo(msg: String) { java.lang.System.out.println(msg) }
7.176 - private def echo_n(msg: String) { java.lang.System.out.print(msg) }
7.177 + /* dependencies */
7.178
7.179 - class Build_Job(cwd: JFile, env: Map[String, String], script: String, args: String)
7.180 + sealed case class Node(
7.181 + loaded_theories: Set[String],
7.182 + sources: List[(Path, SHA1.Digest)])
7.183 +
7.184 + sealed case class Deps(deps: Map[String, Node])
7.185 + {
7.186 + def sources(name: String): List[(Path, SHA1.Digest)] = deps(name).sources
7.187 + }
7.188 +
7.189 + def dependencies(queue: Session.Queue): Deps =
7.190 + Deps((Map.empty[String, Node] /: queue.topological_order)(
7.191 + { case (deps, (name, info)) =>
7.192 + val preloaded =
7.193 + info.parent match {
7.194 + case None => Set.empty[String]
7.195 + case Some(parent) => deps(parent).loaded_theories
7.196 + }
7.197 + val thy_info = new Thy_Info(new Thy_Load(preloaded))
7.198 +
7.199 + val thy_deps =
7.200 + thy_info.dependencies(
7.201 + info.theories.map(_._2).flatten.
7.202 + map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
7.203 +
7.204 + val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
7.205 +
7.206 + val all_files =
7.207 + thy_deps.map({ case (n, h) =>
7.208 + val thy = Path.explode(n.node).expand
7.209 + val uses =
7.210 + h match {
7.211 + case Exn.Res(d) =>
7.212 + d.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
7.213 + case _ => Nil
7.214 + }
7.215 + thy :: uses
7.216 + }).flatten ::: info.files.map(file => info.dir + file)
7.217 + val sources = all_files.par.map(p => (p, SHA1.digest(p))).toList
7.218 +
7.219 + deps + (name -> Node(loaded_theories, sources))
7.220 + }))
7.221 +
7.222 +
7.223 + /* jobs */
7.224 +
7.225 + private class Job(cwd: JFile, env: Map[String, String], script: String, args: String)
7.226 {
7.227 private val args_file = File.tmp_file("args")
7.228 private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
7.229 File.write(args_file, args)
7.230
7.231 - private val (thread, result) = Simple_Thread.future("build_job") {
7.232 - Isabelle_System.bash_env(cwd, env1, script)
7.233 - }
7.234 + private val (thread, result) =
7.235 + Simple_Thread.future("build") { Isabelle_System.bash_env(cwd, env1, script) }
7.236
7.237 def terminate: Unit = thread.interrupt
7.238 def is_finished: Boolean = result.is_finished
7.239 - def join: (String, String, Int) = { val rc = result.join; args_file.delete; rc }
7.240 + def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
7.241 }
7.242
7.243 - private def build_job(save: Boolean, name: String, info: Session.Info): Build_Job =
7.244 + private def start_job(save: Boolean, name: String, info: Session.Info): Job =
7.245 {
7.246 val parent = info.parent.getOrElse("")
7.247
7.248 @@ -300,18 +371,25 @@
7.249 val args_xml =
7.250 {
7.251 import XML.Encode._
7.252 - def symbol_string: T[String] = (s => string(Symbol.encode(s)))
7.253 - pair(bool, pair(symbol_string, pair(symbol_string, list(symbol_string))))(
7.254 - save, (parent, (name, info.theories.map(_._2).flatten)))
7.255 + pair(bool, pair(string, pair(string, list(string))))(
7.256 + save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
7.257 }
7.258 - new Build_Job(cwd, env, script, YXML.string_of_body(args_xml))
7.259 + new Job(cwd, env, script, YXML.string_of_body(args_xml))
7.260 }
7.261
7.262 - def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
7.263 +
7.264 + /* build */
7.265 +
7.266 + private def echo(msg: String) { java.lang.System.out.println(msg) }
7.267 + private def sleep(): Unit = Thread.sleep(500)
7.268 +
7.269 + def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
7.270 + list_only: Boolean, verbose: Boolean,
7.271 more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
7.272 {
7.273 val options = (Options.init() /: more_options)(_.define_simple(_))
7.274 - val queue = find_sessions(all_sessions, sessions, more_dirs)
7.275 + val queue = find_sessions(options, all_sessions, sessions, more_dirs)
7.276 + val deps = dependencies(queue)
7.277
7.278
7.279 // prepare browser info dir
7.280 @@ -331,36 +409,60 @@
7.281 val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
7.282 log_dir.file.mkdirs()
7.283
7.284 - // run jobs
7.285 - val rcs =
7.286 - for ((key, info) <- queue.topological_order) yield
7.287 - {
7.288 - val name = key.name
7.289 + // scheduler loop
7.290 + @tailrec def loop(
7.291 + pending: Session.Queue,
7.292 + running: Map[String, Job],
7.293 + results: Map[String, Int]): Map[String, Int] =
7.294 + {
7.295 + if (pending.is_empty) results
7.296 + else if (running.exists({ case (_, job) => job.is_finished })) {
7.297 + val (name, job) = running.find({ case (_, job) => job.is_finished }).get
7.298
7.299 - if (list_only) { echo(name + " in " + info.dir); 0 }
7.300 + val (out, err, rc) = job.join
7.301 + echo(Library.trim_line(err))
7.302 +
7.303 + val log = log_dir + Path.basic(name)
7.304 + if (rc == 0) {
7.305 + val sources =
7.306 + (queue(name).digest :: deps.sources(name).map(_._2)).map(_.toString).sorted
7.307 + .mkString("sources: ", " ", "\n")
7.308 + File.write_zip(log.ext("gz"), sources + out)
7.309 + }
7.310 else {
7.311 - val save = build_images || queue.is_inner(name)
7.312 - echo((if (save) "Building " else "Running ") + name + " ...")
7.313 -
7.314 - val (out, err, rc) = build_job(save, name, info).join
7.315 - echo_n(err)
7.316 -
7.317 - val log = log_dir + Path.basic(name)
7.318 - if (rc == 0) {
7.319 - File.write_zip(log.ext("gz"), out)
7.320 - }
7.321 - else {
7.322 - File.write(log, out)
7.323 - echo(name + " FAILED")
7.324 - echo("(see also " + log.file + ")")
7.325 - val lines = split_lines(out)
7.326 - val tail = lines.drop(lines.length - 20 max 0)
7.327 - echo("\n" + cat_lines(tail))
7.328 - }
7.329 - rc
7.330 + File.write(log, out)
7.331 + echo(name + " FAILED")
7.332 + echo("(see also " + log.file + ")")
7.333 + val lines = split_lines(out)
7.334 + val tail = lines.drop(lines.length - 20 max 0)
7.335 + echo("\n" + cat_lines(tail))
7.336 + }
7.337 + loop(pending - name, running - name, results + (name -> rc))
7.338 + }
7.339 + else if (running.size < (max_jobs max 1)) {
7.340 + pending.dequeue(running.isDefinedAt(_)) match {
7.341 + case Some((name, info)) =>
7.342 + if (list_only) {
7.343 + echo(name + " in " + info.dir)
7.344 + loop(pending - name, running, results + (name -> 0))
7.345 + }
7.346 + else if (info.parent.map(results(_)).forall(_ == 0)) {
7.347 + val save = build_images || queue.is_inner(name)
7.348 + echo((if (save) "Building " else "Running ") + name + " ...")
7.349 + val job = start_job(save, name, info)
7.350 + loop(pending, running + (name -> job), results)
7.351 + }
7.352 + else {
7.353 + echo(name + " CANCELLED")
7.354 + loop(pending - name, running, results + (name -> 1))
7.355 + }
7.356 + case None => sleep(); loop(pending, running, results)
7.357 }
7.358 }
7.359 - (0 /: rcs)(_ max _)
7.360 + else { sleep(); loop(pending, running, results) }
7.361 + }
7.362 +
7.363 + (0 /: loop(queue, Map.empty, Map.empty))({ case (rc1, (_, rc2)) => rc1 max rc2 })
7.364 }
7.365
7.366
7.367 @@ -373,9 +475,11 @@
7.368 case
7.369 Properties.Value.Boolean(all_sessions) ::
7.370 Properties.Value.Boolean(build_images) ::
7.371 + Properties.Value.Int(max_jobs) ::
7.372 Properties.Value.Boolean(list_only) ::
7.373 + Properties.Value.Boolean(verbose) ::
7.374 Command_Line.Chunks(more_dirs, options, sessions) =>
7.375 - build(all_sessions, build_images, list_only,
7.376 + build(all_sessions, build_images, max_jobs, list_only, verbose,
7.377 more_dirs.map(Path.explode), options, sessions)
7.378 case _ => error("Bad arguments:\n" + cat_lines(args))
7.379 }
8.1 --- a/src/Pure/System/options.scala Sun Jul 22 10:00:51 2012 +0200
8.2 +++ b/src/Pure/System/options.scala Sun Jul 22 23:36:11 2012 +0200
8.3 @@ -12,19 +12,24 @@
8.4
8.5 object Options
8.6 {
8.7 - abstract class Type
8.8 + type Spec = (String, Option[String])
8.9 +
8.10 + val empty: Options = new Options()
8.11 +
8.12 +
8.13 + /* representation */
8.14 +
8.15 + sealed abstract class Type
8.16 {
8.17 def print: String = toString.toLowerCase
8.18 }
8.19 - case object Bool extends Type
8.20 - case object Int extends Type
8.21 - case object Real extends Type
8.22 - case object String extends Type
8.23 + private case object Bool extends Type
8.24 + private case object Int extends Type
8.25 + private case object Real extends Type
8.26 + private case object String extends Type
8.27
8.28 case class Opt(typ: Type, value: String, description: String)
8.29
8.30 - val empty: Options = new Options()
8.31 -
8.32
8.33 /* parsing */
8.34
8.35 @@ -58,7 +63,7 @@
8.36 }
8.37 }
8.38
8.39 - val OPTIONS = Path.explode("etc/options")
8.40 + private val OPTIONS = Path.explode("etc/options")
8.41
8.42 def init(): Options =
8.43 {
8.44 @@ -194,6 +199,9 @@
8.45 }
8.46 }
8.47
8.48 + def ++ (specs: List[Options.Spec]): Options =
8.49 + (this /: specs)({ case (x, (y, z)) => x.define(y, z) })
8.50 +
8.51 def define_simple(str: String): Options =
8.52 {
8.53 str.indexOf('=') match {
9.1 --- a/src/Pure/System/session.scala Sun Jul 22 10:00:51 2012 +0200
9.2 +++ b/src/Pure/System/session.scala Sun Jul 22 23:36:11 2012 +0200
9.3 @@ -37,7 +37,7 @@
9.4 }
9.5
9.6
9.7 -class Session(thy_load: Thy_Load = new Thy_Load)
9.8 +class Session(thy_load: Thy_Load = new Thy_Load())
9.9 {
9.10 /* global flags */
9.11
10.1 --- a/src/Pure/Thy/thy_load.scala Sun Jul 22 10:00:51 2012 +0200
10.2 +++ b/src/Pure/Thy/thy_load.scala Sun Jul 22 23:36:11 2012 +0200
10.3 @@ -10,12 +10,17 @@
10.4 import java.io.{File => JFile}
10.5
10.6
10.7 +object Thy_Load
10.8 +{
10.9 + def thy_path(path: Path): Path = path.ext("thy")
10.10 +}
10.11
10.12 -class Thy_Load
10.13 +
10.14 +class Thy_Load(preloaded: Set[String] = Set.empty)
10.15 {
10.16 /* loaded theories provided by prover */
10.17
10.18 - private var loaded_theories: Set[String] = Set()
10.19 + private var loaded_theories: Set[String] = preloaded
10.20
10.21 def register_thy(thy_name: String): Unit =
10.22 synchronized { loaded_theories += thy_name }
10.23 @@ -39,15 +44,13 @@
10.24
10.25 /* theory files */
10.26
10.27 - def thy_path(path: Path): Path = path.ext("thy")
10.28 -
10.29 private def import_name(dir: String, s: String): Document.Node.Name =
10.30 {
10.31 val theory = Thy_Header.base_name(s)
10.32 if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
10.33 else {
10.34 val path = Path.explode(s)
10.35 - val node = append(dir, thy_path(path))
10.36 + val node = append(dir, Thy_Load.thy_path(path))
10.37 val dir1 = append(dir, path.dir)
10.38 Document.Node.Name(node, dir1, theory)
10.39 }
10.40 @@ -60,7 +63,8 @@
10.41 // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
10.42 val uses = header.uses
10.43 if (name.theory != name1)
10.44 - error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1))
10.45 + error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
10.46 + " for theory " + quote(name1))
10.47 Document.Node.Deps(imports, header.keywords, uses)
10.48 }
10.49
11.1 --- a/src/Pure/library.scala Sun Jul 22 10:00:51 2012 +0200
11.2 +++ b/src/Pure/library.scala Sun Jul 22 23:36:11 2012 +0200
11.3 @@ -62,6 +62,10 @@
11.4
11.5 def split_lines(str: String): List[String] = space_explode('\n', str)
11.6
11.7 + def trim_line(str: String): String =
11.8 + if (str.endsWith("\n")) str.substring(0, str.length - 1)
11.9 + else str
11.10 +
11.11
11.12 /* iterate over chunks (cf. space_explode) */
11.13
12.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala Sun Jul 22 10:00:51 2012 +0200
12.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala Sun Jul 22 23:36:11 2012 +0200
12.3 @@ -17,7 +17,7 @@
12.4 import org.gjt.sp.jedit.View
12.5
12.6
12.7 -class JEdit_Thy_Load extends Thy_Load
12.8 +class JEdit_Thy_Load extends Thy_Load()
12.9 {
12.10 override def append(dir: String, source_path: Path): String =
12.11 {