merged
authorwenzelm
Sun, 22 Jul 2012 23:36:11 +0200
changeset 494444b7f4482c552
parent 49443 ffa0618cc4d4
parent 49440 0d95980e9aae
child 49445 6cbfe187a0f9
merged
     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    {