moved files;
authorwenzelm
Wed Jan 02 17:58:53 2013 +0100 (2013-01-02)
changeset 50686d703e3aafa8c
parent 50685 293e8ec4dfc8
child 50687 a8db4bf70e90
moved files;
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/build.ML
src/Pure/System/build.scala
src/Pure/System/build_dialog.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/Tools/build_dialog.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/ROOT	Wed Jan 02 16:48:22 2013 +0100
     1.2 +++ b/src/Pure/ROOT	Wed Jan 02 17:58:53 2013 +0100
     1.3 @@ -181,7 +181,6 @@
     1.4      "Syntax/syntax_phases.ML"
     1.5      "Syntax/syntax_trans.ML"
     1.6      "Syntax/term_position.ML"
     1.7 -    "System/build.ML"
     1.8      "System/command_line.ML"
     1.9      "System/invoke_scala.ML"
    1.10      "System/isabelle_process.ML"
    1.11 @@ -201,6 +200,7 @@
    1.12      "Thy/thy_load.ML"
    1.13      "Thy/thy_output.ML"
    1.14      "Thy/thy_syntax.ML"
    1.15 +    "Tools/build.ML"
    1.16      "Tools/named_thms.ML"
    1.17      "Tools/legacy_xml_syntax.ML"
    1.18      "assumption.ML"
     2.1 --- a/src/Pure/ROOT.ML	Wed Jan 02 16:48:22 2013 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Wed Jan 02 17:58:53 2013 +0100
     2.3 @@ -276,7 +276,6 @@
     2.4  
     2.5  use "System/session.ML";
     2.6  use "System/command_line.ML";
     2.7 -use "System/build.ML";
     2.8  use "System/system_channel.ML";
     2.9  use "System/isabelle_process.ML";
    2.10  use "System/invoke_scala.ML";
    2.11 @@ -286,8 +285,8 @@
    2.12  
    2.13  (* miscellaneous tools and packages for Pure Isabelle *)
    2.14  
    2.15 +use "Tools/build.ML";
    2.16  use "Tools/named_thms.ML";
    2.17 -
    2.18  use "Tools/legacy_xml_syntax.ML";
    2.19  
    2.20  
     3.1 --- a/src/Pure/System/build.ML	Wed Jan 02 16:48:22 2013 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,117 +0,0 @@
     3.4 -(*  Title:      Pure/System/build.ML
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -Build Isabelle sessions.
     3.8 -*)
     3.9 -
    3.10 -signature BUILD =
    3.11 -sig
    3.12 -  val build: string -> unit
    3.13 -end;
    3.14 -
    3.15 -structure Build: BUILD =
    3.16 -struct
    3.17 -
    3.18 -(* protocol messages *)
    3.19 -
    3.20 -fun ML_statistics (function :: stats) "" =
    3.21 -      if function = Markup.ML_statistics then SOME stats
    3.22 -      else NONE
    3.23 -  | ML_statistics _ _ = NONE;
    3.24 -
    3.25 -fun protocol_message props output =
    3.26 -  (case ML_statistics props output of
    3.27 -    SOME stats =>
    3.28 -      writeln ("\f" ^ #2 Markup.ML_statistics ^ " = " ^ ML_Syntax.print_properties stats)
    3.29 -  | NONE => raise Fail "Undefined Output.protocol_message");
    3.30 -
    3.31 -
    3.32 -(* build *)
    3.33 -
    3.34 -local
    3.35 -
    3.36 -fun no_document options =
    3.37 -  (case Options.string options "document" of "" => true | "false" => true | _ => false);
    3.38 -
    3.39 -fun use_thys options =
    3.40 -  Thy_Info.use_thys
    3.41 -    |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    3.42 -    |> Unsynchronized.setmp print_mode
    3.43 -        (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    3.44 -    |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    3.45 -    |> Unsynchronized.setmp Goal.parallel_proofs_threshold
    3.46 -        (Options.int options "parallel_proofs_threshold")
    3.47 -    |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    3.48 -    |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    3.49 -    |> Unsynchronized.setmp Future.ML_statistics (Options.bool options "ML_statistics")
    3.50 -    |> no_document options ? Present.no_document
    3.51 -    |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    3.52 -    |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
    3.53 -    |> Unsynchronized.setmp Printer.show_question_marks_default
    3.54 -        (Options.bool options "show_question_marks")
    3.55 -    |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    3.56 -    |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
    3.57 -    |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
    3.58 -    |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
    3.59 -    |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
    3.60 -    |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
    3.61 -    |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
    3.62 -    |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
    3.63 -    |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    3.64 -    |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    3.65 -
    3.66 -fun use_theories (options, thys) =
    3.67 -  let val condition = space_explode "," (Options.string options "condition") in
    3.68 -    (case filter_out (can getenv_strict) condition of
    3.69 -      [] => use_thys options (map (rpair Position.none) thys)
    3.70 -    | conds =>
    3.71 -        Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    3.72 -          " (undefined " ^ commas conds ^ ")\n"))
    3.73 -  end;
    3.74 -
    3.75 -in
    3.76 -
    3.77 -fun build args_file = Command_Line.tool (fn () =>
    3.78 -    let
    3.79 -      val (do_output, (options, (verbose, (browser_info, (parent_name,
    3.80 -          (name, theories)))))) =
    3.81 -        File.read (Path.explode args_file) |> YXML.parse_body |>
    3.82 -          let open XML.Decode in
    3.83 -            pair bool (pair Options.decode (pair bool (pair string (pair string
    3.84 -              (pair string ((list (pair Options.decode (list string)))))))))
    3.85 -          end;
    3.86 -
    3.87 -      val document_variants =
    3.88 -        map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
    3.89 -      val _ =
    3.90 -        (case duplicates (op =) (map fst document_variants) of
    3.91 -          [] => ()
    3.92 -        | dups => error ("Duplicate document variants: " ^ commas_quote dups));
    3.93 -
    3.94 -      val _ =
    3.95 -        Session.init do_output false
    3.96 -          (Options.bool options "browser_info") browser_info
    3.97 -          (Options.string options "document")
    3.98 -          (Options.bool options "document_graph")
    3.99 -          (Options.string options "document_output")
   3.100 -          document_variants
   3.101 -          parent_name name
   3.102 -          (false, "") ""
   3.103 -          verbose;
   3.104 -
   3.105 -      val res1 =
   3.106 -        theories |>
   3.107 -          (List.app use_theories
   3.108 -            |> Session.with_timing name verbose
   3.109 -            |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
   3.110 -            |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
   3.111 -            |> Exn.capture);
   3.112 -      val res2 = Exn.capture Session.finish ();
   3.113 -      val _ = Par_Exn.release_all [res1, res2];
   3.114 -
   3.115 -      val _ = if do_output then () else exit 0;
   3.116 -    in 0 end);
   3.117 -
   3.118 -end;
   3.119 -
   3.120 -end;
     4.1 --- a/src/Pure/System/build.scala	Wed Jan 02 16:48:22 2013 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,750 +0,0 @@
     4.4 -/*  Title:      Pure/System/build.scala
     4.5 -    Author:     Makarius
     4.6 -    Options:    :folding=explicit:collapseFolds=1:
     4.7 -
     4.8 -Build and manage Isabelle sessions.
     4.9 -*/
    4.10 -
    4.11 -package isabelle
    4.12 -
    4.13 -
    4.14 -import java.util.{Timer, TimerTask}
    4.15 -import java.io.{BufferedInputStream, FileInputStream,
    4.16 -  BufferedReader, InputStreamReader, IOException}
    4.17 -import java.util.zip.GZIPInputStream
    4.18 -
    4.19 -import scala.collection.SortedSet
    4.20 -import scala.annotation.tailrec
    4.21 -
    4.22 -
    4.23 -object Build
    4.24 -{
    4.25 -  /** progress context **/
    4.26 -
    4.27 -  class Progress {
    4.28 -    def echo(msg: String) {}
    4.29 -    def stopped: Boolean = false
    4.30 -  }
    4.31 -
    4.32 -  object Ignore_Progress extends Progress
    4.33 -
    4.34 -  object Console_Progress extends Progress {
    4.35 -    override def echo(msg: String) { java.lang.System.out.println(msg) }
    4.36 -  }
    4.37 -
    4.38 -
    4.39 -
    4.40 -  /** session information **/
    4.41 -
    4.42 -  // external version
    4.43 -  sealed case class Session_Entry(
    4.44 -    pos: Position.T,
    4.45 -    name: String,
    4.46 -    groups: List[String],
    4.47 -    path: String,
    4.48 -    parent: Option[String],
    4.49 -    description: String,
    4.50 -    options: List[Options.Spec],
    4.51 -    theories: List[(List[Options.Spec], List[String])],
    4.52 -    files: List[String])
    4.53 -
    4.54 -  // internal version
    4.55 -  sealed case class Session_Info(
    4.56 -    select: Boolean,
    4.57 -    pos: Position.T,
    4.58 -    groups: List[String],
    4.59 -    dir: Path,
    4.60 -    parent: Option[String],
    4.61 -    description: String,
    4.62 -    options: Options,
    4.63 -    theories: List[(Options, List[Path])],
    4.64 -    files: List[Path],
    4.65 -    entry_digest: SHA1.Digest)
    4.66 -
    4.67 -  def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
    4.68 -
    4.69 -  def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
    4.70 -      : (String, Session_Info) =
    4.71 -    try {
    4.72 -      val name = entry.name
    4.73 -
    4.74 -      if (name == "") error("Bad session name")
    4.75 -      if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
    4.76 -      if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
    4.77 -
    4.78 -      val session_options = options ++ entry.options
    4.79 -
    4.80 -      val theories =
    4.81 -        entry.theories.map({ case (opts, thys) =>
    4.82 -          (session_options ++ opts, thys.map(Path.explode(_))) })
    4.83 -      val files = entry.files.map(Path.explode(_))
    4.84 -      val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString)
    4.85 -
    4.86 -      val info =
    4.87 -        Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path),
    4.88 -          entry.parent, entry.description, session_options, theories, files, entry_digest)
    4.89 -
    4.90 -      (name, info)
    4.91 -    }
    4.92 -    catch {
    4.93 -      case ERROR(msg) =>
    4.94 -        error(msg + "\nThe error(s) above occurred in session entry " +
    4.95 -          quote(entry.name) + Position.here(entry.pos))
    4.96 -    }
    4.97 -
    4.98 -
    4.99 -  /* session tree */
   4.100 -
   4.101 -  object Session_Tree
   4.102 -  {
   4.103 -    def apply(infos: Seq[(String, Session_Info)]): Session_Tree =
   4.104 -    {
   4.105 -      val graph1 =
   4.106 -        (Graph.string[Session_Info] /: infos) {
   4.107 -          case (graph, (name, info)) =>
   4.108 -            if (graph.defined(name))
   4.109 -              error("Duplicate session " + quote(name) + Position.here(info.pos))
   4.110 -            else graph.new_node(name, info)
   4.111 -        }
   4.112 -      val graph2 =
   4.113 -        (graph1 /: graph1.entries) {
   4.114 -          case (graph, (name, (info, _))) =>
   4.115 -            info.parent match {
   4.116 -              case None => graph
   4.117 -              case Some(parent) =>
   4.118 -                if (!graph.defined(parent))
   4.119 -                  error("Bad parent session " + quote(parent) + " for " +
   4.120 -                    quote(name) + Position.here(info.pos))
   4.121 -
   4.122 -                try { graph.add_edge_acyclic(parent, name) }
   4.123 -                catch {
   4.124 -                  case exn: Graph.Cycles[_] =>
   4.125 -                    error(cat_lines(exn.cycles.map(cycle =>
   4.126 -                      "Cyclic session dependency of " +
   4.127 -                        cycle.map(c => quote(c.toString)).mkString(" via "))) +
   4.128 -                          Position.here(info.pos))
   4.129 -                }
   4.130 -            }
   4.131 -        }
   4.132 -      new Session_Tree(graph2)
   4.133 -    }
   4.134 -  }
   4.135 -
   4.136 -  final class Session_Tree private(val graph: Graph[String, Session_Info])
   4.137 -    extends PartialFunction[String, Session_Info]
   4.138 -  {
   4.139 -    def apply(name: String): Session_Info = graph.get_node(name)
   4.140 -    def isDefinedAt(name: String): Boolean = graph.defined(name)
   4.141 -
   4.142 -    def selection(requirements: Boolean, all_sessions: Boolean,
   4.143 -      session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) =
   4.144 -    {
   4.145 -      val bad_sessions = sessions.filterNot(isDefinedAt(_))
   4.146 -      if (!bad_sessions.isEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
   4.147 -
   4.148 -      val pre_selected =
   4.149 -      {
   4.150 -        if (all_sessions) graph.keys.toList
   4.151 -        else {
   4.152 -          val select_group = session_groups.toSet
   4.153 -          val select = sessions.toSet
   4.154 -          (for {
   4.155 -            (name, (info, _)) <- graph.entries
   4.156 -            if info.select || select(name) || apply(name).groups.exists(select_group)
   4.157 -          } yield name).toList
   4.158 -        }
   4.159 -      }
   4.160 -      val selected =
   4.161 -        if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
   4.162 -        else pre_selected
   4.163 -
   4.164 -      val tree1 = new Session_Tree(graph.restrict(graph.all_preds(selected).toSet))
   4.165 -      (selected, tree1)
   4.166 -    }
   4.167 -
   4.168 -    def topological_order: List[(String, Session_Info)] =
   4.169 -      graph.topological_order.map(name => (name, apply(name)))
   4.170 -
   4.171 -    override def toString: String = graph.entries.map(_._1).toList.sorted.mkString(",")
   4.172 -  }
   4.173 -
   4.174 -
   4.175 -  /* parser */
   4.176 -
   4.177 -  private val SESSION = "session"
   4.178 -  private val IN = "in"
   4.179 -  private val DESCRIPTION = "description"
   4.180 -  private val OPTIONS = "options"
   4.181 -  private val THEORIES = "theories"
   4.182 -  private val FILES = "files"
   4.183 -
   4.184 -  lazy val root_syntax =
   4.185 -    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   4.186 -      (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
   4.187 -
   4.188 -  private object Parser extends Parse.Parser
   4.189 -  {
   4.190 -    def session_entry(pos: Position.T): Parser[Session_Entry] =
   4.191 -    {
   4.192 -      val session_name = atom("session name", _.is_name)
   4.193 -
   4.194 -      val option =
   4.195 -        name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   4.196 -      val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]")
   4.197 -
   4.198 -      val theories =
   4.199 -        keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
   4.200 -          { case _ ~ (x ~ y) => (x, y) }
   4.201 -
   4.202 -      command(SESSION) ~!
   4.203 -        (session_name ~
   4.204 -          ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
   4.205 -          ((keyword(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
   4.206 -          (keyword("=") ~!
   4.207 -            (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~
   4.208 -              ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
   4.209 -              ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
   4.210 -              rep1(theories) ~
   4.211 -              ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
   4.212 -        { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
   4.213 -            Session_Entry(pos, a, b, c, d, e, f, g, h) }
   4.214 -    }
   4.215 -
   4.216 -    def parse_entries(root: Path): List[Session_Entry] =
   4.217 -    {
   4.218 -      val toks = root_syntax.scan(File.read(root))
   4.219 -      parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
   4.220 -        case Success(result, _) => result
   4.221 -        case bad => error(bad.toString)
   4.222 -      }
   4.223 -    }
   4.224 -  }
   4.225 -
   4.226 -
   4.227 -  /* find sessions within certain directories */
   4.228 -
   4.229 -  private val ROOT = Path.explode("ROOT")
   4.230 -  private val ROOTS = Path.explode("ROOTS")
   4.231 -
   4.232 -  private def is_session_dir(dir: Path): Boolean =
   4.233 -    (dir + ROOT).is_file || (dir + ROOTS).is_file
   4.234 -
   4.235 -  private def check_session_dir(dir: Path): Path =
   4.236 -    if (is_session_dir(dir)) dir
   4.237 -    else error("Bad session root directory: " + dir.toString)
   4.238 -
   4.239 -  def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree =
   4.240 -  {
   4.241 -    def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
   4.242 -      find_root(select, dir) ::: find_roots(select, dir)
   4.243 -
   4.244 -    def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
   4.245 -    {
   4.246 -      val root = dir + ROOT
   4.247 -      if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _))
   4.248 -      else Nil
   4.249 -    }
   4.250 -
   4.251 -    def find_roots(select: Boolean, dir: Path): List[(String, Session_Info)] =
   4.252 -    {
   4.253 -      val roots = dir + ROOTS
   4.254 -      if (roots.is_file) {
   4.255 -        for {
   4.256 -          line <- split_lines(File.read(roots))
   4.257 -          if !(line == "" || line.startsWith("#"))
   4.258 -          dir1 =
   4.259 -            try { check_session_dir(dir + Path.explode(line)) }
   4.260 -            catch {
   4.261 -              case ERROR(msg) =>
   4.262 -                error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
   4.263 -            }
   4.264 -          info <- find_dir(select, dir1)
   4.265 -        } yield info
   4.266 -      }
   4.267 -      else Nil
   4.268 -    }
   4.269 -
   4.270 -    val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _))
   4.271 -
   4.272 -    more_dirs foreach { case (_, dir) => check_session_dir(dir) }
   4.273 -
   4.274 -    Session_Tree(
   4.275 -      for {
   4.276 -        (select, dir) <- default_dirs ::: more_dirs
   4.277 -        info <- find_dir(select, dir)
   4.278 -      } yield info)
   4.279 -  }
   4.280 -
   4.281 -
   4.282 -
   4.283 -  /** build **/
   4.284 -
   4.285 -  /* queue */
   4.286 -
   4.287 -  object Queue
   4.288 -  {
   4.289 -    def apply(tree: Session_Tree): Queue =
   4.290 -    {
   4.291 -      val graph = tree.graph
   4.292 -
   4.293 -      def outdegree(name: String): Int = graph.imm_succs(name).size
   4.294 -      def timeout(name: String): Double = tree(name).options.real("timeout")
   4.295 -
   4.296 -      object Ordering extends scala.math.Ordering[String]
   4.297 -      {
   4.298 -        def compare(name1: String, name2: String): Int =
   4.299 -          outdegree(name2) compare outdegree(name1) match {
   4.300 -            case 0 =>
   4.301 -              timeout(name2) compare timeout(name1) match {
   4.302 -                case 0 => name1 compare name2
   4.303 -                case ord => ord
   4.304 -              }
   4.305 -            case ord => ord
   4.306 -          }
   4.307 -      }
   4.308 -
   4.309 -      new Queue(graph, SortedSet(graph.keys.toList: _*)(Ordering))
   4.310 -    }
   4.311 -  }
   4.312 -
   4.313 -  final class Queue private(graph: Graph[String, Session_Info], order: SortedSet[String])
   4.314 -  {
   4.315 -    def is_inner(name: String): Boolean = !graph.is_maximal(name)
   4.316 -
   4.317 -    def is_empty: Boolean = graph.is_empty
   4.318 -
   4.319 -    def - (name: String): Queue = new Queue(graph.del_node(name), order - name)
   4.320 -
   4.321 -    def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
   4.322 -    {
   4.323 -      val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
   4.324 -      if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
   4.325 -      else None
   4.326 -    }
   4.327 -  }
   4.328 -
   4.329 -
   4.330 -  /* source dependencies and static content */
   4.331 -
   4.332 -  sealed case class Session_Content(
   4.333 -    loaded_theories: Set[String],
   4.334 -    syntax: Outer_Syntax,
   4.335 -    sources: List[(Path, SHA1.Digest)],
   4.336 -    errors: List[String])
   4.337 -  {
   4.338 -    def check_errors: Session_Content =
   4.339 -    {
   4.340 -      if (errors.isEmpty) this
   4.341 -      else error(cat_lines(errors))
   4.342 -    }
   4.343 -  }
   4.344 -
   4.345 -  sealed case class Deps(deps: Map[String, Session_Content])
   4.346 -  {
   4.347 -    def is_empty: Boolean = deps.isEmpty
   4.348 -    def apply(name: String): Session_Content = deps(name)
   4.349 -    def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   4.350 -  }
   4.351 -
   4.352 -  def dependencies(progress: Build.Progress, inlined_files: Boolean,
   4.353 -      verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
   4.354 -    Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
   4.355 -      { case (deps, (name, info)) =>
   4.356 -          val (preloaded, parent_syntax, parent_errors) =
   4.357 -            info.parent match {
   4.358 -              case None =>
   4.359 -                (Set.empty[String], Outer_Syntax.init_pure(), Nil)
   4.360 -              case Some(parent_name) =>
   4.361 -                val parent = deps(parent_name)
   4.362 -                (parent.loaded_theories, parent.syntax, parent.errors)
   4.363 -            }
   4.364 -          val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
   4.365 -
   4.366 -          if (verbose || list_files) {
   4.367 -            val groups =
   4.368 -              if (info.groups.isEmpty) ""
   4.369 -              else info.groups.mkString(" (", " ", ")")
   4.370 -            progress.echo("Session " + name + groups)
   4.371 -          }
   4.372 -
   4.373 -          val thy_deps =
   4.374 -            thy_info.dependencies(inlined_files,
   4.375 -              info.theories.map(_._2).flatten.
   4.376 -                map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
   4.377 -
   4.378 -          val loaded_theories = thy_deps.loaded_theories
   4.379 -          val syntax = thy_deps.make_syntax
   4.380 -
   4.381 -          val all_files =
   4.382 -            (thy_deps.deps.map({ case dep =>
   4.383 -              val thy = Path.explode(dep.name.node)
   4.384 -              val uses = dep.join_header.uses.map(p =>
   4.385 -                Path.explode(dep.name.dir) + Path.explode(p._1))
   4.386 -              thy :: uses
   4.387 -            }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
   4.388 -
   4.389 -          if (list_files)
   4.390 -            progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
   4.391 -
   4.392 -          val sources =
   4.393 -            try { all_files.map(p => (p, SHA1.digest(p.file))) }
   4.394 -            catch {
   4.395 -              case ERROR(msg) =>
   4.396 -                error(msg + "\nThe error(s) above occurred in session " +
   4.397 -                  quote(name) + Position.here(info.pos))
   4.398 -            }
   4.399 -          val errors = parent_errors ::: thy_deps.deps.map(dep => dep.join_header.errors).flatten
   4.400 -
   4.401 -          deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
   4.402 -      }))
   4.403 -
   4.404 -  def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
   4.405 -  {
   4.406 -    val options = Options.init()
   4.407 -    val (_, tree) =
   4.408 -      find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, List(session))
   4.409 -    dependencies(Build.Ignore_Progress, inlined_files, false, false, tree)(session)
   4.410 -  }
   4.411 -
   4.412 -  def outer_syntax(session: String): Outer_Syntax =
   4.413 -    session_content(false, Nil, session).check_errors.syntax
   4.414 -
   4.415 -
   4.416 -  /* jobs */
   4.417 -
   4.418 -  private class Job(name: String, info: Session_Info, output: Path, do_output: Boolean,
   4.419 -    verbose: Boolean, browser_info: Path)
   4.420 -  {
   4.421 -    // global browser info dir
   4.422 -    if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
   4.423 -    {
   4.424 -      browser_info.file.mkdirs()
   4.425 -      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
   4.426 -        browser_info + Path.explode("isabelle.gif"))
   4.427 -      File.write(browser_info + Path.explode("index.html"),
   4.428 -        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
   4.429 -        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
   4.430 -        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
   4.431 -    }
   4.432 -
   4.433 -    def output_path: Option[Path] = if (do_output) Some(output) else None
   4.434 -
   4.435 -    private val parent = info.parent.getOrElse("")
   4.436 -
   4.437 -    private val args_file = File.tmp_file("args")
   4.438 -    File.write(args_file, YXML.string_of_body(
   4.439 -      if (is_pure(name)) Options.encode(info.options)
   4.440 -      else
   4.441 -        {
   4.442 -          import XML.Encode._
   4.443 -              pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
   4.444 -                pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
   4.445 -              (do_output, (info.options, (verbose, (browser_info, (parent,
   4.446 -                (name, info.theories)))))))
   4.447 -        }))
   4.448 -
   4.449 -    private val env =
   4.450 -      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
   4.451 -        (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
   4.452 -          Isabelle_System.posix_path(args_file.getPath))
   4.453 -
   4.454 -    private val script =
   4.455 -      if (is_pure(name)) {
   4.456 -        if (do_output) "./build " + name + " \"$OUTPUT\""
   4.457 -        else """ rm -f "$OUTPUT"; ./build """ + name
   4.458 -      }
   4.459 -      else {
   4.460 -        """
   4.461 -        . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   4.462 -        """ +
   4.463 -          (if (do_output)
   4.464 -            """
   4.465 -            "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT"
   4.466 -            """
   4.467 -          else
   4.468 -            """
   4.469 -            rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT"
   4.470 -            """) +
   4.471 -        """
   4.472 -        RC="$?"
   4.473 -
   4.474 -        . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   4.475 -
   4.476 -        if [ "$RC" -eq 0 ]; then
   4.477 -          echo "Finished $TARGET ($TIMES_REPORT)" >&2
   4.478 -        fi
   4.479 -
   4.480 -        exit "$RC"
   4.481 -        """
   4.482 -      }
   4.483 -
   4.484 -    private val (thread, result) =
   4.485 -      Simple_Thread.future("build") { Isabelle_System.bash_env(info.dir.file, env, script) }
   4.486 -
   4.487 -    def terminate: Unit = thread.interrupt
   4.488 -    def is_finished: Boolean = result.is_finished
   4.489 -
   4.490 -    @volatile private var timeout = false
   4.491 -    private val time = info.options.seconds("timeout")
   4.492 -    private val timer: Option[Timer] =
   4.493 -      if (time.seconds > 0.0) {
   4.494 -        val t = new Timer("build", true)
   4.495 -        t.schedule(new TimerTask { def run = { terminate; timeout = true } }, time.ms)
   4.496 -        Some(t)
   4.497 -      }
   4.498 -      else None
   4.499 -
   4.500 -    def join: (String, String, Int) = {
   4.501 -      val (out, err, rc) = result.join
   4.502 -      args_file.delete
   4.503 -      timer.map(_.cancel())
   4.504 -
   4.505 -      val err1 =
   4.506 -        if (rc == 130)
   4.507 -          (if (err.isEmpty || err.endsWith("\n")) err else err + "\n") +
   4.508 -          (if (timeout) "*** Timeout\n" else "*** Interrupt\n")
   4.509 -        else err
   4.510 -      (out, err1, rc)
   4.511 -    }
   4.512 -  }
   4.513 -
   4.514 -
   4.515 -  /* log files and corresponding heaps */
   4.516 -
   4.517 -  private val LOG = Path.explode("log")
   4.518 -  private def log(name: String): Path = LOG + Path.basic(name)
   4.519 -  private def log_gz(name: String): Path = log(name).ext("gz")
   4.520 -
   4.521 -  private def sources_stamp(digests: List[SHA1.Digest]): String =
   4.522 -    digests.map(_.toString).sorted.mkString("sources: ", " ", "")
   4.523 -
   4.524 -  private val no_heap: String = "heap: -"
   4.525 -
   4.526 -  private def heap_stamp(heap: Option[Path]): String =
   4.527 -  {
   4.528 -    "heap: " +
   4.529 -      (heap match {
   4.530 -        case Some(path) =>
   4.531 -          val file = path.file
   4.532 -          if (file.isFile) file.length.toString + " " + file.lastModified.toString
   4.533 -          else "-"
   4.534 -        case None => "-"
   4.535 -      })
   4.536 -  }
   4.537 -
   4.538 -  private def read_stamps(path: Path): Option[(String, String, String)] =
   4.539 -    if (path.is_file) {
   4.540 -      val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(path.file)))
   4.541 -      val reader = new BufferedReader(new InputStreamReader(stream, UTF8.charset))
   4.542 -      val (s, h1, h2) =
   4.543 -        try { (reader.readLine, reader.readLine, reader.readLine) }
   4.544 -        finally { reader.close }
   4.545 -      if (s != null && s.startsWith("sources: ") &&
   4.546 -          h1 != null && h1.startsWith("heap: ") &&
   4.547 -          h2 != null && h2.startsWith("heap: ")) Some((s, h1, h2))
   4.548 -      else None
   4.549 -    }
   4.550 -    else None
   4.551 -
   4.552 -
   4.553 -  /* build */
   4.554 -
   4.555 -  def build(
   4.556 -    progress: Build.Progress,
   4.557 -    options: Options,
   4.558 -    requirements: Boolean = false,
   4.559 -    all_sessions: Boolean = false,
   4.560 -    build_heap: Boolean = false,
   4.561 -    clean_build: Boolean = false,
   4.562 -    more_dirs: List[(Boolean, Path)] = Nil,
   4.563 -    session_groups: List[String] = Nil,
   4.564 -    max_jobs: Int = 1,
   4.565 -    list_files: Boolean = false,
   4.566 -    no_build: Boolean = false,
   4.567 -    system_mode: Boolean = false,
   4.568 -    verbose: Boolean = false,
   4.569 -    sessions: List[String] = Nil): Int =
   4.570 -  {
   4.571 -    val full_tree = find_sessions(options, more_dirs)
   4.572 -    val (selected, selected_tree) =
   4.573 -      full_tree.selection(requirements, all_sessions, session_groups, sessions)
   4.574 -
   4.575 -    val deps = dependencies(progress, true, verbose, list_files, selected_tree)
   4.576 -    val queue = Queue(selected_tree)
   4.577 -
   4.578 -    def make_stamp(name: String): String =
   4.579 -      sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
   4.580 -
   4.581 -    val (input_dirs, output_dir, browser_info) =
   4.582 -      if (system_mode) {
   4.583 -        val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
   4.584 -        (List(output_dir), output_dir, Path.explode("~~/browser_info"))
   4.585 -      }
   4.586 -      else {
   4.587 -        val output_dir = Path.explode("$ISABELLE_OUTPUT")
   4.588 -        (output_dir :: Isabelle_System.find_logics_dirs(), output_dir,
   4.589 -         Path.explode("$ISABELLE_BROWSER_INFO"))
   4.590 -      }
   4.591 -
   4.592 -    // prepare log dir
   4.593 -    (output_dir + LOG).file.mkdirs()
   4.594 -
   4.595 -    // optional cleanup
   4.596 -    if (clean_build) {
   4.597 -      for (name <- full_tree.graph.all_succs(selected)) {
   4.598 -        val files =
   4.599 -          List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
   4.600 -        if (!files.isEmpty) progress.echo("Cleaning " + name + " ...")
   4.601 -        if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
   4.602 -      }
   4.603 -    }
   4.604 -
   4.605 -    // scheduler loop
   4.606 -    case class Result(current: Boolean, heap: String, rc: Int)
   4.607 -
   4.608 -    def sleep(): Unit = Thread.sleep(500)
   4.609 -
   4.610 -    @tailrec def loop(
   4.611 -      pending: Queue,
   4.612 -      running: Map[String, (String, Job)],
   4.613 -      results: Map[String, Result]): Map[String, Result] =
   4.614 -    {
   4.615 -      if (pending.is_empty) results
   4.616 -      else if (progress.stopped) {
   4.617 -        for ((_, (_, job)) <- running) job.terminate
   4.618 -        sleep(); loop(pending, running, results)
   4.619 -      }
   4.620 -      else
   4.621 -        running.find({ case (_, (_, job)) => job.is_finished }) match {
   4.622 -          case Some((name, (parent_heap, job))) =>
   4.623 -            //{{{ finish job
   4.624 -
   4.625 -            val (out, err, rc) = job.join
   4.626 -            progress.echo(Library.trim_line(err))
   4.627 -
   4.628 -            val heap =
   4.629 -              if (rc == 0) {
   4.630 -                (output_dir + log(name)).file.delete
   4.631 -
   4.632 -                val sources = make_stamp(name)
   4.633 -                val heap = heap_stamp(job.output_path)
   4.634 -                File.write_gzip(output_dir + log_gz(name),
   4.635 -                  sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
   4.636 -
   4.637 -                heap
   4.638 -              }
   4.639 -              else {
   4.640 -                (output_dir + Path.basic(name)).file.delete
   4.641 -                (output_dir + log_gz(name)).file.delete
   4.642 -
   4.643 -                File.write(output_dir + log(name), out)
   4.644 -                progress.echo(name + " FAILED")
   4.645 -                if (rc != 130) {
   4.646 -                  progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
   4.647 -                  val lines = split_lines(out)
   4.648 -                  val tail = lines.drop(lines.length - 20 max 0)
   4.649 -                  progress.echo("\n" + cat_lines(tail))
   4.650 -                }
   4.651 -
   4.652 -                no_heap
   4.653 -              }
   4.654 -            loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
   4.655 -            //}}}
   4.656 -          case None if (running.size < (max_jobs max 1)) =>
   4.657 -            //{{{ check/start next job
   4.658 -            pending.dequeue(running.isDefinedAt(_)) match {
   4.659 -              case Some((name, info)) =>
   4.660 -                val parent_result =
   4.661 -                  info.parent match {
   4.662 -                    case None => Result(true, no_heap, 0)
   4.663 -                    case Some(parent) => results(parent)
   4.664 -                  }
   4.665 -                val output = output_dir + Path.basic(name)
   4.666 -                val do_output = build_heap || queue.is_inner(name)
   4.667 -
   4.668 -                val (current, heap) =
   4.669 -                {
   4.670 -                  input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
   4.671 -                    case Some(dir) =>
   4.672 -                      read_stamps(dir + log_gz(name)) match {
   4.673 -                        case Some((s, h1, h2)) =>
   4.674 -                          val heap = heap_stamp(Some(dir + Path.basic(name)))
   4.675 -                          (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
   4.676 -                            !(do_output && heap == no_heap), heap)
   4.677 -                        case None => (false, no_heap)
   4.678 -                      }
   4.679 -                    case None => (false, no_heap)
   4.680 -                  }
   4.681 -                }
   4.682 -                val all_current = current && parent_result.current
   4.683 -
   4.684 -                if (all_current)
   4.685 -                  loop(pending - name, running, results + (name -> Result(true, heap, 0)))
   4.686 -                else if (no_build) {
   4.687 -                  if (verbose) progress.echo("Skipping " + name + " ...")
   4.688 -                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   4.689 -                }
   4.690 -                else if (parent_result.rc == 0) {
   4.691 -                  progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   4.692 -                  val job = new Job(name, info, output, do_output, verbose, browser_info)
   4.693 -                  loop(pending, running + (name -> (parent_result.heap, job)), results)
   4.694 -                }
   4.695 -                else {
   4.696 -                  progress.echo(name + " CANCELLED")
   4.697 -                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   4.698 -                }
   4.699 -              case None => sleep(); loop(pending, running, results)
   4.700 -            }
   4.701 -            ///}}}
   4.702 -          case None => sleep(); loop(pending, running, results)
   4.703 -        }
   4.704 -    }
   4.705 -
   4.706 -    val results =
   4.707 -      if (deps.is_empty) {
   4.708 -        progress.echo("### Nothing to build")
   4.709 -        Map.empty
   4.710 -      }
   4.711 -      else loop(queue, Map.empty, Map.empty)
   4.712 -
   4.713 -    val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
   4.714 -    if (rc != 0 && (verbose || !no_build)) {
   4.715 -      val unfinished =
   4.716 -        (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList
   4.717 -          .sorted(scala.math.Ordering.String)  // FIXME scala-2.10.0-RC1
   4.718 -      progress.echo("Unfinished session(s): " + commas(unfinished))
   4.719 -    }
   4.720 -    rc
   4.721 -  }
   4.722 -
   4.723 -
   4.724 -  /* command line entry point */
   4.725 -
   4.726 -  def main(args: Array[String])
   4.727 -  {
   4.728 -    Command_Line.tool {
   4.729 -      args.toList match {
   4.730 -        case
   4.731 -          Properties.Value.Boolean(requirements) ::
   4.732 -          Properties.Value.Boolean(all_sessions) ::
   4.733 -          Properties.Value.Boolean(build_heap) ::
   4.734 -          Properties.Value.Boolean(clean_build) ::
   4.735 -          Properties.Value.Int(max_jobs) ::
   4.736 -          Properties.Value.Boolean(list_files) ::
   4.737 -          Properties.Value.Boolean(no_build) ::
   4.738 -          Properties.Value.Boolean(system_mode) ::
   4.739 -          Properties.Value.Boolean(verbose) ::
   4.740 -          Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
   4.741 -            val options = (Options.init() /: build_options)(_ + _)
   4.742 -            val dirs =
   4.743 -              select_dirs.map(d => (true, Path.explode(d))) :::
   4.744 -              include_dirs.map(d => (false, Path.explode(d)))
   4.745 -            build(Build.Console_Progress, options, requirements, all_sessions, build_heap,
   4.746 -              clean_build, dirs, session_groups, max_jobs, list_files, no_build, system_mode,
   4.747 -              verbose, sessions)
   4.748 -        case _ => error("Bad arguments:\n" + cat_lines(args))
   4.749 -      }
   4.750 -    }
   4.751 -  }
   4.752 -}
   4.753 -
     5.1 --- a/src/Pure/System/build_dialog.scala	Wed Jan 02 16:48:22 2013 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,135 +0,0 @@
     5.4 -/*  Title:      Pure/System/build_dialog.scala
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Dialog for session build process.
     5.8 -*/
     5.9 -
    5.10 -package isabelle
    5.11 -
    5.12 -
    5.13 -import java.awt.{GraphicsEnvironment, Point, Font}
    5.14 -
    5.15 -import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
    5.16 -  BorderPanel, MainFrame, TextArea, SwingApplication}
    5.17 -import scala.swing.event.ButtonClicked
    5.18 -
    5.19 -
    5.20 -object Build_Dialog
    5.21 -{
    5.22 -  def main(args: Array[String]) =
    5.23 -  {
    5.24 -    Platform.init_laf()
    5.25 -    try {
    5.26 -      args.toList match {
    5.27 -        case
    5.28 -          logic_option ::
    5.29 -          logic ::
    5.30 -          Properties.Value.Boolean(system_mode) ::
    5.31 -          include_dirs =>
    5.32 -            val more_dirs = include_dirs.map(s => ((false, Path.explode(s))))
    5.33 -
    5.34 -            val options = Options.init()
    5.35 -            val session =
    5.36 -              Isabelle_System.default_logic(logic,
    5.37 -                if (logic_option != "") options.string(logic_option) else "")
    5.38 -
    5.39 -            if (Build.build(Build.Ignore_Progress, options, build_heap = true, no_build = true,
    5.40 -                more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0)
    5.41 -            else
    5.42 -              Swing_Thread.later {
    5.43 -                val top = build_dialog(options, system_mode, more_dirs, session)
    5.44 -                top.pack()
    5.45 -
    5.46 -                val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
    5.47 -                top.location =
    5.48 -                  new Point(point.x - top.size.width / 2, point.y - top.size.height / 2)
    5.49 -
    5.50 -                top.visible = true
    5.51 -              }
    5.52 -        case _ => error("Bad arguments:\n" + cat_lines(args))
    5.53 -      }
    5.54 -    }
    5.55 -    catch {
    5.56 -      case exn: Throwable =>
    5.57 -        Library.error_dialog(null, "Isabelle build failure",
    5.58 -          Library.scrollable_text(Exn.message(exn)))
    5.59 -        sys.exit(2)
    5.60 -    }
    5.61 -  }
    5.62 -
    5.63 -
    5.64 -  def build_dialog(
    5.65 -    options: Options,
    5.66 -    system_mode: Boolean,
    5.67 -    more_dirs: List[(Boolean, Path)],
    5.68 -    session: String): MainFrame = new MainFrame
    5.69 -  {
    5.70 -    /* GUI state */
    5.71 -
    5.72 -    private var is_stopped = false
    5.73 -    private var return_code = 0
    5.74 -
    5.75 -
    5.76 -    /* text */
    5.77 -
    5.78 -    val text = new TextArea {
    5.79 -      font = new Font("SansSerif", Font.PLAIN, 14)
    5.80 -      editable = false
    5.81 -      columns = 40
    5.82 -      rows = 10
    5.83 -    }
    5.84 -
    5.85 -    val progress = new Build.Progress
    5.86 -    {
    5.87 -      override def echo(msg: String): Unit = Swing_Thread.now { text.append(msg + "\n") }
    5.88 -      override def stopped: Boolean =
    5.89 -        Swing_Thread.now { val b = is_stopped; is_stopped = false; b  }
    5.90 -    }
    5.91 -
    5.92 -
    5.93 -    /* action button */
    5.94 -
    5.95 -    var button_action: () => Unit = (() => is_stopped = true)
    5.96 -    val button = new Button("Cancel") {
    5.97 -      reactions += { case ButtonClicked(_) => button_action() }
    5.98 -    }
    5.99 -    def button_exit(rc: Int)
   5.100 -    {
   5.101 -      button.text = if (rc == 0) "OK" else "Exit"
   5.102 -      button_action = (() => sys.exit(rc))
   5.103 -      button.peer.getRootPane.setDefaultButton(button.peer)
   5.104 -    }
   5.105 -
   5.106 -    val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button)
   5.107 -
   5.108 -
   5.109 -    /* layout panel */
   5.110 -
   5.111 -    val layout_panel = new BorderPanel
   5.112 -    layout_panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
   5.113 -    layout_panel.layout(action_panel) = BorderPanel.Position.South
   5.114 -
   5.115 -    contents = layout_panel
   5.116 -
   5.117 -
   5.118 -    /* main build */
   5.119 -
   5.120 -    title = "Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")"
   5.121 -    progress.echo("Build started for Isabelle/" + session + " ...")
   5.122 -
   5.123 -    default_thread_pool.submit(() => {
   5.124 -      val (out, rc) =
   5.125 -        try {
   5.126 -          ("",
   5.127 -            Build.build(progress, options, build_heap = true, more_dirs = more_dirs,
   5.128 -              system_mode = system_mode, sessions = List(session)))
   5.129 -        }
   5.130 -        catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
   5.131 -      Swing_Thread.now {
   5.132 -        progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
   5.133 -        button_exit(rc)
   5.134 -      }
   5.135 -    })
   5.136 -  }
   5.137 -}
   5.138 -
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/Tools/build.ML	Wed Jan 02 17:58:53 2013 +0100
     6.3 @@ -0,0 +1,117 @@
     6.4 +(*  Title:      Pure/Tools/build.ML
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Build Isabelle sessions.
     6.8 +*)
     6.9 +
    6.10 +signature BUILD =
    6.11 +sig
    6.12 +  val build: string -> unit
    6.13 +end;
    6.14 +
    6.15 +structure Build: BUILD =
    6.16 +struct
    6.17 +
    6.18 +(* protocol messages *)
    6.19 +
    6.20 +fun ML_statistics (function :: stats) "" =
    6.21 +      if function = Markup.ML_statistics then SOME stats
    6.22 +      else NONE
    6.23 +  | ML_statistics _ _ = NONE;
    6.24 +
    6.25 +fun protocol_message props output =
    6.26 +  (case ML_statistics props output of
    6.27 +    SOME stats =>
    6.28 +      writeln ("\f" ^ #2 Markup.ML_statistics ^ " = " ^ ML_Syntax.print_properties stats)
    6.29 +  | NONE => raise Fail "Undefined Output.protocol_message");
    6.30 +
    6.31 +
    6.32 +(* build *)
    6.33 +
    6.34 +local
    6.35 +
    6.36 +fun no_document options =
    6.37 +  (case Options.string options "document" of "" => true | "false" => true | _ => false);
    6.38 +
    6.39 +fun use_thys options =
    6.40 +  Thy_Info.use_thys
    6.41 +    |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    6.42 +    |> Unsynchronized.setmp print_mode
    6.43 +        (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    6.44 +    |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    6.45 +    |> Unsynchronized.setmp Goal.parallel_proofs_threshold
    6.46 +        (Options.int options "parallel_proofs_threshold")
    6.47 +    |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    6.48 +    |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    6.49 +    |> Unsynchronized.setmp Future.ML_statistics (Options.bool options "ML_statistics")
    6.50 +    |> no_document options ? Present.no_document
    6.51 +    |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    6.52 +    |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
    6.53 +    |> Unsynchronized.setmp Printer.show_question_marks_default
    6.54 +        (Options.bool options "show_question_marks")
    6.55 +    |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    6.56 +    |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
    6.57 +    |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
    6.58 +    |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
    6.59 +    |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
    6.60 +    |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
    6.61 +    |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
    6.62 +    |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
    6.63 +    |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    6.64 +    |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    6.65 +
    6.66 +fun use_theories (options, thys) =
    6.67 +  let val condition = space_explode "," (Options.string options "condition") in
    6.68 +    (case filter_out (can getenv_strict) condition of
    6.69 +      [] => use_thys options (map (rpair Position.none) thys)
    6.70 +    | conds =>
    6.71 +        Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    6.72 +          " (undefined " ^ commas conds ^ ")\n"))
    6.73 +  end;
    6.74 +
    6.75 +in
    6.76 +
    6.77 +fun build args_file = Command_Line.tool (fn () =>
    6.78 +    let
    6.79 +      val (do_output, (options, (verbose, (browser_info, (parent_name,
    6.80 +          (name, theories)))))) =
    6.81 +        File.read (Path.explode args_file) |> YXML.parse_body |>
    6.82 +          let open XML.Decode in
    6.83 +            pair bool (pair Options.decode (pair bool (pair string (pair string
    6.84 +              (pair string ((list (pair Options.decode (list string)))))))))
    6.85 +          end;
    6.86 +
    6.87 +      val document_variants =
    6.88 +        map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
    6.89 +      val _ =
    6.90 +        (case duplicates (op =) (map fst document_variants) of
    6.91 +          [] => ()
    6.92 +        | dups => error ("Duplicate document variants: " ^ commas_quote dups));
    6.93 +
    6.94 +      val _ =
    6.95 +        Session.init do_output false
    6.96 +          (Options.bool options "browser_info") browser_info
    6.97 +          (Options.string options "document")
    6.98 +          (Options.bool options "document_graph")
    6.99 +          (Options.string options "document_output")
   6.100 +          document_variants
   6.101 +          parent_name name
   6.102 +          (false, "") ""
   6.103 +          verbose;
   6.104 +
   6.105 +      val res1 =
   6.106 +        theories |>
   6.107 +          (List.app use_theories
   6.108 +            |> Session.with_timing name verbose
   6.109 +            |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
   6.110 +            |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
   6.111 +            |> Exn.capture);
   6.112 +      val res2 = Exn.capture Session.finish ();
   6.113 +      val _ = Par_Exn.release_all [res1, res2];
   6.114 +
   6.115 +      val _ = if do_output then () else exit 0;
   6.116 +    in 0 end);
   6.117 +
   6.118 +end;
   6.119 +
   6.120 +end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/Tools/build.scala	Wed Jan 02 17:58:53 2013 +0100
     7.3 @@ -0,0 +1,750 @@
     7.4 +/*  Title:      Pure/Tools/build.scala
     7.5 +    Author:     Makarius
     7.6 +    Options:    :folding=explicit:collapseFolds=1:
     7.7 +
     7.8 +Build and manage Isabelle sessions.
     7.9 +*/
    7.10 +
    7.11 +package isabelle
    7.12 +
    7.13 +
    7.14 +import java.util.{Timer, TimerTask}
    7.15 +import java.io.{BufferedInputStream, FileInputStream,
    7.16 +  BufferedReader, InputStreamReader, IOException}
    7.17 +import java.util.zip.GZIPInputStream
    7.18 +
    7.19 +import scala.collection.SortedSet
    7.20 +import scala.annotation.tailrec
    7.21 +
    7.22 +
    7.23 +object Build
    7.24 +{
    7.25 +  /** progress context **/
    7.26 +
    7.27 +  class Progress {
    7.28 +    def echo(msg: String) {}
    7.29 +    def stopped: Boolean = false
    7.30 +  }
    7.31 +
    7.32 +  object Ignore_Progress extends Progress
    7.33 +
    7.34 +  object Console_Progress extends Progress {
    7.35 +    override def echo(msg: String) { java.lang.System.out.println(msg) }
    7.36 +  }
    7.37 +
    7.38 +
    7.39 +
    7.40 +  /** session information **/
    7.41 +
    7.42 +  // external version
    7.43 +  sealed case class Session_Entry(
    7.44 +    pos: Position.T,
    7.45 +    name: String,
    7.46 +    groups: List[String],
    7.47 +    path: String,
    7.48 +    parent: Option[String],
    7.49 +    description: String,
    7.50 +    options: List[Options.Spec],
    7.51 +    theories: List[(List[Options.Spec], List[String])],
    7.52 +    files: List[String])
    7.53 +
    7.54 +  // internal version
    7.55 +  sealed case class Session_Info(
    7.56 +    select: Boolean,
    7.57 +    pos: Position.T,
    7.58 +    groups: List[String],
    7.59 +    dir: Path,
    7.60 +    parent: Option[String],
    7.61 +    description: String,
    7.62 +    options: Options,
    7.63 +    theories: List[(Options, List[Path])],
    7.64 +    files: List[Path],
    7.65 +    entry_digest: SHA1.Digest)
    7.66 +
    7.67 +  def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
    7.68 +
    7.69 +  def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
    7.70 +      : (String, Session_Info) =
    7.71 +    try {
    7.72 +      val name = entry.name
    7.73 +
    7.74 +      if (name == "") error("Bad session name")
    7.75 +      if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
    7.76 +      if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
    7.77 +
    7.78 +      val session_options = options ++ entry.options
    7.79 +
    7.80 +      val theories =
    7.81 +        entry.theories.map({ case (opts, thys) =>
    7.82 +          (session_options ++ opts, thys.map(Path.explode(_))) })
    7.83 +      val files = entry.files.map(Path.explode(_))
    7.84 +      val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString)
    7.85 +
    7.86 +      val info =
    7.87 +        Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path),
    7.88 +          entry.parent, entry.description, session_options, theories, files, entry_digest)
    7.89 +
    7.90 +      (name, info)
    7.91 +    }
    7.92 +    catch {
    7.93 +      case ERROR(msg) =>
    7.94 +        error(msg + "\nThe error(s) above occurred in session entry " +
    7.95 +          quote(entry.name) + Position.here(entry.pos))
    7.96 +    }
    7.97 +
    7.98 +
    7.99 +  /* session tree */
   7.100 +
   7.101 +  object Session_Tree
   7.102 +  {
   7.103 +    def apply(infos: Seq[(String, Session_Info)]): Session_Tree =
   7.104 +    {
   7.105 +      val graph1 =
   7.106 +        (Graph.string[Session_Info] /: infos) {
   7.107 +          case (graph, (name, info)) =>
   7.108 +            if (graph.defined(name))
   7.109 +              error("Duplicate session " + quote(name) + Position.here(info.pos))
   7.110 +            else graph.new_node(name, info)
   7.111 +        }
   7.112 +      val graph2 =
   7.113 +        (graph1 /: graph1.entries) {
   7.114 +          case (graph, (name, (info, _))) =>
   7.115 +            info.parent match {
   7.116 +              case None => graph
   7.117 +              case Some(parent) =>
   7.118 +                if (!graph.defined(parent))
   7.119 +                  error("Bad parent session " + quote(parent) + " for " +
   7.120 +                    quote(name) + Position.here(info.pos))
   7.121 +
   7.122 +                try { graph.add_edge_acyclic(parent, name) }
   7.123 +                catch {
   7.124 +                  case exn: Graph.Cycles[_] =>
   7.125 +                    error(cat_lines(exn.cycles.map(cycle =>
   7.126 +                      "Cyclic session dependency of " +
   7.127 +                        cycle.map(c => quote(c.toString)).mkString(" via "))) +
   7.128 +                          Position.here(info.pos))
   7.129 +                }
   7.130 +            }
   7.131 +        }
   7.132 +      new Session_Tree(graph2)
   7.133 +    }
   7.134 +  }
   7.135 +
   7.136 +  final class Session_Tree private(val graph: Graph[String, Session_Info])
   7.137 +    extends PartialFunction[String, Session_Info]
   7.138 +  {
   7.139 +    def apply(name: String): Session_Info = graph.get_node(name)
   7.140 +    def isDefinedAt(name: String): Boolean = graph.defined(name)
   7.141 +
   7.142 +    def selection(requirements: Boolean, all_sessions: Boolean,
   7.143 +      session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) =
   7.144 +    {
   7.145 +      val bad_sessions = sessions.filterNot(isDefinedAt(_))
   7.146 +      if (!bad_sessions.isEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
   7.147 +
   7.148 +      val pre_selected =
   7.149 +      {
   7.150 +        if (all_sessions) graph.keys.toList
   7.151 +        else {
   7.152 +          val select_group = session_groups.toSet
   7.153 +          val select = sessions.toSet
   7.154 +          (for {
   7.155 +            (name, (info, _)) <- graph.entries
   7.156 +            if info.select || select(name) || apply(name).groups.exists(select_group)
   7.157 +          } yield name).toList
   7.158 +        }
   7.159 +      }
   7.160 +      val selected =
   7.161 +        if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
   7.162 +        else pre_selected
   7.163 +
   7.164 +      val tree1 = new Session_Tree(graph.restrict(graph.all_preds(selected).toSet))
   7.165 +      (selected, tree1)
   7.166 +    }
   7.167 +
   7.168 +    def topological_order: List[(String, Session_Info)] =
   7.169 +      graph.topological_order.map(name => (name, apply(name)))
   7.170 +
   7.171 +    override def toString: String = graph.entries.map(_._1).toList.sorted.mkString(",")
   7.172 +  }
   7.173 +
   7.174 +
   7.175 +  /* parser */
   7.176 +
   7.177 +  private val SESSION = "session"
   7.178 +  private val IN = "in"
   7.179 +  private val DESCRIPTION = "description"
   7.180 +  private val OPTIONS = "options"
   7.181 +  private val THEORIES = "theories"
   7.182 +  private val FILES = "files"
   7.183 +
   7.184 +  lazy val root_syntax =
   7.185 +    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   7.186 +      (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
   7.187 +
   7.188 +  private object Parser extends Parse.Parser
   7.189 +  {
   7.190 +    def session_entry(pos: Position.T): Parser[Session_Entry] =
   7.191 +    {
   7.192 +      val session_name = atom("session name", _.is_name)
   7.193 +
   7.194 +      val option =
   7.195 +        name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   7.196 +      val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]")
   7.197 +
   7.198 +      val theories =
   7.199 +        keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
   7.200 +          { case _ ~ (x ~ y) => (x, y) }
   7.201 +
   7.202 +      command(SESSION) ~!
   7.203 +        (session_name ~
   7.204 +          ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
   7.205 +          ((keyword(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
   7.206 +          (keyword("=") ~!
   7.207 +            (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~
   7.208 +              ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
   7.209 +              ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
   7.210 +              rep1(theories) ~
   7.211 +              ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
   7.212 +        { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
   7.213 +            Session_Entry(pos, a, b, c, d, e, f, g, h) }
   7.214 +    }
   7.215 +
   7.216 +    def parse_entries(root: Path): List[Session_Entry] =
   7.217 +    {
   7.218 +      val toks = root_syntax.scan(File.read(root))
   7.219 +      parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
   7.220 +        case Success(result, _) => result
   7.221 +        case bad => error(bad.toString)
   7.222 +      }
   7.223 +    }
   7.224 +  }
   7.225 +
   7.226 +
   7.227 +  /* find sessions within certain directories */
   7.228 +
   7.229 +  private val ROOT = Path.explode("ROOT")
   7.230 +  private val ROOTS = Path.explode("ROOTS")
   7.231 +
   7.232 +  private def is_session_dir(dir: Path): Boolean =
   7.233 +    (dir + ROOT).is_file || (dir + ROOTS).is_file
   7.234 +
   7.235 +  private def check_session_dir(dir: Path): Path =
   7.236 +    if (is_session_dir(dir)) dir
   7.237 +    else error("Bad session root directory: " + dir.toString)
   7.238 +
   7.239 +  def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree =
   7.240 +  {
   7.241 +    def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
   7.242 +      find_root(select, dir) ::: find_roots(select, dir)
   7.243 +
   7.244 +    def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
   7.245 +    {
   7.246 +      val root = dir + ROOT
   7.247 +      if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _))
   7.248 +      else Nil
   7.249 +    }
   7.250 +
   7.251 +    def find_roots(select: Boolean, dir: Path): List[(String, Session_Info)] =
   7.252 +    {
   7.253 +      val roots = dir + ROOTS
   7.254 +      if (roots.is_file) {
   7.255 +        for {
   7.256 +          line <- split_lines(File.read(roots))
   7.257 +          if !(line == "" || line.startsWith("#"))
   7.258 +          dir1 =
   7.259 +            try { check_session_dir(dir + Path.explode(line)) }
   7.260 +            catch {
   7.261 +              case ERROR(msg) =>
   7.262 +                error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
   7.263 +            }
   7.264 +          info <- find_dir(select, dir1)
   7.265 +        } yield info
   7.266 +      }
   7.267 +      else Nil
   7.268 +    }
   7.269 +
   7.270 +    val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _))
   7.271 +
   7.272 +    more_dirs foreach { case (_, dir) => check_session_dir(dir) }
   7.273 +
   7.274 +    Session_Tree(
   7.275 +      for {
   7.276 +        (select, dir) <- default_dirs ::: more_dirs
   7.277 +        info <- find_dir(select, dir)
   7.278 +      } yield info)
   7.279 +  }
   7.280 +
   7.281 +
   7.282 +
   7.283 +  /** build **/
   7.284 +
   7.285 +  /* queue */
   7.286 +
   7.287 +  object Queue
   7.288 +  {
   7.289 +    def apply(tree: Session_Tree): Queue =
   7.290 +    {
   7.291 +      val graph = tree.graph
   7.292 +
   7.293 +      def outdegree(name: String): Int = graph.imm_succs(name).size
   7.294 +      def timeout(name: String): Double = tree(name).options.real("timeout")
   7.295 +
   7.296 +      object Ordering extends scala.math.Ordering[String]
   7.297 +      {
   7.298 +        def compare(name1: String, name2: String): Int =
   7.299 +          outdegree(name2) compare outdegree(name1) match {
   7.300 +            case 0 =>
   7.301 +              timeout(name2) compare timeout(name1) match {
   7.302 +                case 0 => name1 compare name2
   7.303 +                case ord => ord
   7.304 +              }
   7.305 +            case ord => ord
   7.306 +          }
   7.307 +      }
   7.308 +
   7.309 +      new Queue(graph, SortedSet(graph.keys.toList: _*)(Ordering))
   7.310 +    }
   7.311 +  }
   7.312 +
   7.313 +  final class Queue private(graph: Graph[String, Session_Info], order: SortedSet[String])
   7.314 +  {
   7.315 +    def is_inner(name: String): Boolean = !graph.is_maximal(name)
   7.316 +
   7.317 +    def is_empty: Boolean = graph.is_empty
   7.318 +
   7.319 +    def - (name: String): Queue = new Queue(graph.del_node(name), order - name)
   7.320 +
   7.321 +    def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
   7.322 +    {
   7.323 +      val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
   7.324 +      if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
   7.325 +      else None
   7.326 +    }
   7.327 +  }
   7.328 +
   7.329 +
   7.330 +  /* source dependencies and static content */
   7.331 +
   7.332 +  sealed case class Session_Content(
   7.333 +    loaded_theories: Set[String],
   7.334 +    syntax: Outer_Syntax,
   7.335 +    sources: List[(Path, SHA1.Digest)],
   7.336 +    errors: List[String])
   7.337 +  {
   7.338 +    def check_errors: Session_Content =
   7.339 +    {
   7.340 +      if (errors.isEmpty) this
   7.341 +      else error(cat_lines(errors))
   7.342 +    }
   7.343 +  }
   7.344 +
   7.345 +  sealed case class Deps(deps: Map[String, Session_Content])
   7.346 +  {
   7.347 +    def is_empty: Boolean = deps.isEmpty
   7.348 +    def apply(name: String): Session_Content = deps(name)
   7.349 +    def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   7.350 +  }
   7.351 +
   7.352 +  def dependencies(progress: Build.Progress, inlined_files: Boolean,
   7.353 +      verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
   7.354 +    Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
   7.355 +      { case (deps, (name, info)) =>
   7.356 +          val (preloaded, parent_syntax, parent_errors) =
   7.357 +            info.parent match {
   7.358 +              case None =>
   7.359 +                (Set.empty[String], Outer_Syntax.init_pure(), Nil)
   7.360 +              case Some(parent_name) =>
   7.361 +                val parent = deps(parent_name)
   7.362 +                (parent.loaded_theories, parent.syntax, parent.errors)
   7.363 +            }
   7.364 +          val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
   7.365 +
   7.366 +          if (verbose || list_files) {
   7.367 +            val groups =
   7.368 +              if (info.groups.isEmpty) ""
   7.369 +              else info.groups.mkString(" (", " ", ")")
   7.370 +            progress.echo("Session " + name + groups)
   7.371 +          }
   7.372 +
   7.373 +          val thy_deps =
   7.374 +            thy_info.dependencies(inlined_files,
   7.375 +              info.theories.map(_._2).flatten.
   7.376 +                map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
   7.377 +
   7.378 +          val loaded_theories = thy_deps.loaded_theories
   7.379 +          val syntax = thy_deps.make_syntax
   7.380 +
   7.381 +          val all_files =
   7.382 +            (thy_deps.deps.map({ case dep =>
   7.383 +              val thy = Path.explode(dep.name.node)
   7.384 +              val uses = dep.join_header.uses.map(p =>
   7.385 +                Path.explode(dep.name.dir) + Path.explode(p._1))
   7.386 +              thy :: uses
   7.387 +            }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
   7.388 +
   7.389 +          if (list_files)
   7.390 +            progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
   7.391 +
   7.392 +          val sources =
   7.393 +            try { all_files.map(p => (p, SHA1.digest(p.file))) }
   7.394 +            catch {
   7.395 +              case ERROR(msg) =>
   7.396 +                error(msg + "\nThe error(s) above occurred in session " +
   7.397 +                  quote(name) + Position.here(info.pos))
   7.398 +            }
   7.399 +          val errors = parent_errors ::: thy_deps.deps.map(dep => dep.join_header.errors).flatten
   7.400 +
   7.401 +          deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
   7.402 +      }))
   7.403 +
   7.404 +  def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
   7.405 +  {
   7.406 +    val options = Options.init()
   7.407 +    val (_, tree) =
   7.408 +      find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, List(session))
   7.409 +    dependencies(Build.Ignore_Progress, inlined_files, false, false, tree)(session)
   7.410 +  }
   7.411 +
   7.412 +  def outer_syntax(session: String): Outer_Syntax =
   7.413 +    session_content(false, Nil, session).check_errors.syntax
   7.414 +
   7.415 +
   7.416 +  /* jobs */
   7.417 +
   7.418 +  private class Job(name: String, info: Session_Info, output: Path, do_output: Boolean,
   7.419 +    verbose: Boolean, browser_info: Path)
   7.420 +  {
   7.421 +    // global browser info dir
   7.422 +    if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
   7.423 +    {
   7.424 +      browser_info.file.mkdirs()
   7.425 +      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
   7.426 +        browser_info + Path.explode("isabelle.gif"))
   7.427 +      File.write(browser_info + Path.explode("index.html"),
   7.428 +        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
   7.429 +        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
   7.430 +        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
   7.431 +    }
   7.432 +
   7.433 +    def output_path: Option[Path] = if (do_output) Some(output) else None
   7.434 +
   7.435 +    private val parent = info.parent.getOrElse("")
   7.436 +
   7.437 +    private val args_file = File.tmp_file("args")
   7.438 +    File.write(args_file, YXML.string_of_body(
   7.439 +      if (is_pure(name)) Options.encode(info.options)
   7.440 +      else
   7.441 +        {
   7.442 +          import XML.Encode._
   7.443 +              pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
   7.444 +                pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
   7.445 +              (do_output, (info.options, (verbose, (browser_info, (parent,
   7.446 +                (name, info.theories)))))))
   7.447 +        }))
   7.448 +
   7.449 +    private val env =
   7.450 +      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
   7.451 +        (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
   7.452 +          Isabelle_System.posix_path(args_file.getPath))
   7.453 +
   7.454 +    private val script =
   7.455 +      if (is_pure(name)) {
   7.456 +        if (do_output) "./build " + name + " \"$OUTPUT\""
   7.457 +        else """ rm -f "$OUTPUT"; ./build """ + name
   7.458 +      }
   7.459 +      else {
   7.460 +        """
   7.461 +        . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   7.462 +        """ +
   7.463 +          (if (do_output)
   7.464 +            """
   7.465 +            "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT"
   7.466 +            """
   7.467 +          else
   7.468 +            """
   7.469 +            rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT"
   7.470 +            """) +
   7.471 +        """
   7.472 +        RC="$?"
   7.473 +
   7.474 +        . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   7.475 +
   7.476 +        if [ "$RC" -eq 0 ]; then
   7.477 +          echo "Finished $TARGET ($TIMES_REPORT)" >&2
   7.478 +        fi
   7.479 +
   7.480 +        exit "$RC"
   7.481 +        """
   7.482 +      }
   7.483 +
   7.484 +    private val (thread, result) =
   7.485 +      Simple_Thread.future("build") { Isabelle_System.bash_env(info.dir.file, env, script) }
   7.486 +
   7.487 +    def terminate: Unit = thread.interrupt
   7.488 +    def is_finished: Boolean = result.is_finished
   7.489 +
   7.490 +    @volatile private var timeout = false
   7.491 +    private val time = info.options.seconds("timeout")
   7.492 +    private val timer: Option[Timer] =
   7.493 +      if (time.seconds > 0.0) {
   7.494 +        val t = new Timer("build", true)
   7.495 +        t.schedule(new TimerTask { def run = { terminate; timeout = true } }, time.ms)
   7.496 +        Some(t)
   7.497 +      }
   7.498 +      else None
   7.499 +
   7.500 +    def join: (String, String, Int) = {
   7.501 +      val (out, err, rc) = result.join
   7.502 +      args_file.delete
   7.503 +      timer.map(_.cancel())
   7.504 +
   7.505 +      val err1 =
   7.506 +        if (rc == 130)
   7.507 +          (if (err.isEmpty || err.endsWith("\n")) err else err + "\n") +
   7.508 +          (if (timeout) "*** Timeout\n" else "*** Interrupt\n")
   7.509 +        else err
   7.510 +      (out, err1, rc)
   7.511 +    }
   7.512 +  }
   7.513 +
   7.514 +
   7.515 +  /* log files and corresponding heaps */
   7.516 +
   7.517 +  private val LOG = Path.explode("log")
   7.518 +  private def log(name: String): Path = LOG + Path.basic(name)
   7.519 +  private def log_gz(name: String): Path = log(name).ext("gz")
   7.520 +
   7.521 +  private def sources_stamp(digests: List[SHA1.Digest]): String =
   7.522 +    digests.map(_.toString).sorted.mkString("sources: ", " ", "")
   7.523 +
   7.524 +  private val no_heap: String = "heap: -"
   7.525 +
   7.526 +  private def heap_stamp(heap: Option[Path]): String =
   7.527 +  {
   7.528 +    "heap: " +
   7.529 +      (heap match {
   7.530 +        case Some(path) =>
   7.531 +          val file = path.file
   7.532 +          if (file.isFile) file.length.toString + " " + file.lastModified.toString
   7.533 +          else "-"
   7.534 +        case None => "-"
   7.535 +      })
   7.536 +  }
   7.537 +
   7.538 +  private def read_stamps(path: Path): Option[(String, String, String)] =
   7.539 +    if (path.is_file) {
   7.540 +      val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(path.file)))
   7.541 +      val reader = new BufferedReader(new InputStreamReader(stream, UTF8.charset))
   7.542 +      val (s, h1, h2) =
   7.543 +        try { (reader.readLine, reader.readLine, reader.readLine) }
   7.544 +        finally { reader.close }
   7.545 +      if (s != null && s.startsWith("sources: ") &&
   7.546 +          h1 != null && h1.startsWith("heap: ") &&
   7.547 +          h2 != null && h2.startsWith("heap: ")) Some((s, h1, h2))
   7.548 +      else None
   7.549 +    }
   7.550 +    else None
   7.551 +
   7.552 +
   7.553 +  /* build */
   7.554 +
   7.555 +  def build(
   7.556 +    progress: Build.Progress,
   7.557 +    options: Options,
   7.558 +    requirements: Boolean = false,
   7.559 +    all_sessions: Boolean = false,
   7.560 +    build_heap: Boolean = false,
   7.561 +    clean_build: Boolean = false,
   7.562 +    more_dirs: List[(Boolean, Path)] = Nil,
   7.563 +    session_groups: List[String] = Nil,
   7.564 +    max_jobs: Int = 1,
   7.565 +    list_files: Boolean = false,
   7.566 +    no_build: Boolean = false,
   7.567 +    system_mode: Boolean = false,
   7.568 +    verbose: Boolean = false,
   7.569 +    sessions: List[String] = Nil): Int =
   7.570 +  {
   7.571 +    val full_tree = find_sessions(options, more_dirs)
   7.572 +    val (selected, selected_tree) =
   7.573 +      full_tree.selection(requirements, all_sessions, session_groups, sessions)
   7.574 +
   7.575 +    val deps = dependencies(progress, true, verbose, list_files, selected_tree)
   7.576 +    val queue = Queue(selected_tree)
   7.577 +
   7.578 +    def make_stamp(name: String): String =
   7.579 +      sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
   7.580 +
   7.581 +    val (input_dirs, output_dir, browser_info) =
   7.582 +      if (system_mode) {
   7.583 +        val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
   7.584 +        (List(output_dir), output_dir, Path.explode("~~/browser_info"))
   7.585 +      }
   7.586 +      else {
   7.587 +        val output_dir = Path.explode("$ISABELLE_OUTPUT")
   7.588 +        (output_dir :: Isabelle_System.find_logics_dirs(), output_dir,
   7.589 +         Path.explode("$ISABELLE_BROWSER_INFO"))
   7.590 +      }
   7.591 +
   7.592 +    // prepare log dir
   7.593 +    (output_dir + LOG).file.mkdirs()
   7.594 +
   7.595 +    // optional cleanup
   7.596 +    if (clean_build) {
   7.597 +      for (name <- full_tree.graph.all_succs(selected)) {
   7.598 +        val files =
   7.599 +          List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
   7.600 +        if (!files.isEmpty) progress.echo("Cleaning " + name + " ...")
   7.601 +        if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
   7.602 +      }
   7.603 +    }
   7.604 +
   7.605 +    // scheduler loop
   7.606 +    case class Result(current: Boolean, heap: String, rc: Int)
   7.607 +
   7.608 +    def sleep(): Unit = Thread.sleep(500)
   7.609 +
   7.610 +    @tailrec def loop(
   7.611 +      pending: Queue,
   7.612 +      running: Map[String, (String, Job)],
   7.613 +      results: Map[String, Result]): Map[String, Result] =
   7.614 +    {
   7.615 +      if (pending.is_empty) results
   7.616 +      else if (progress.stopped) {
   7.617 +        for ((_, (_, job)) <- running) job.terminate
   7.618 +        sleep(); loop(pending, running, results)
   7.619 +      }
   7.620 +      else
   7.621 +        running.find({ case (_, (_, job)) => job.is_finished }) match {
   7.622 +          case Some((name, (parent_heap, job))) =>
   7.623 +            //{{{ finish job
   7.624 +
   7.625 +            val (out, err, rc) = job.join
   7.626 +            progress.echo(Library.trim_line(err))
   7.627 +
   7.628 +            val heap =
   7.629 +              if (rc == 0) {
   7.630 +                (output_dir + log(name)).file.delete
   7.631 +
   7.632 +                val sources = make_stamp(name)
   7.633 +                val heap = heap_stamp(job.output_path)
   7.634 +                File.write_gzip(output_dir + log_gz(name),
   7.635 +                  sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
   7.636 +
   7.637 +                heap
   7.638 +              }
   7.639 +              else {
   7.640 +                (output_dir + Path.basic(name)).file.delete
   7.641 +                (output_dir + log_gz(name)).file.delete
   7.642 +
   7.643 +                File.write(output_dir + log(name), out)
   7.644 +                progress.echo(name + " FAILED")
   7.645 +                if (rc != 130) {
   7.646 +                  progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
   7.647 +                  val lines = split_lines(out)
   7.648 +                  val tail = lines.drop(lines.length - 20 max 0)
   7.649 +                  progress.echo("\n" + cat_lines(tail))
   7.650 +                }
   7.651 +
   7.652 +                no_heap
   7.653 +              }
   7.654 +            loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
   7.655 +            //}}}
   7.656 +          case None if (running.size < (max_jobs max 1)) =>
   7.657 +            //{{{ check/start next job
   7.658 +            pending.dequeue(running.isDefinedAt(_)) match {
   7.659 +              case Some((name, info)) =>
   7.660 +                val parent_result =
   7.661 +                  info.parent match {
   7.662 +                    case None => Result(true, no_heap, 0)
   7.663 +                    case Some(parent) => results(parent)
   7.664 +                  }
   7.665 +                val output = output_dir + Path.basic(name)
   7.666 +                val do_output = build_heap || queue.is_inner(name)
   7.667 +
   7.668 +                val (current, heap) =
   7.669 +                {
   7.670 +                  input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
   7.671 +                    case Some(dir) =>
   7.672 +                      read_stamps(dir + log_gz(name)) match {
   7.673 +                        case Some((s, h1, h2)) =>
   7.674 +                          val heap = heap_stamp(Some(dir + Path.basic(name)))
   7.675 +                          (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
   7.676 +                            !(do_output && heap == no_heap), heap)
   7.677 +                        case None => (false, no_heap)
   7.678 +                      }
   7.679 +                    case None => (false, no_heap)
   7.680 +                  }
   7.681 +                }
   7.682 +                val all_current = current && parent_result.current
   7.683 +
   7.684 +                if (all_current)
   7.685 +                  loop(pending - name, running, results + (name -> Result(true, heap, 0)))
   7.686 +                else if (no_build) {
   7.687 +                  if (verbose) progress.echo("Skipping " + name + " ...")
   7.688 +                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   7.689 +                }
   7.690 +                else if (parent_result.rc == 0) {
   7.691 +                  progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   7.692 +                  val job = new Job(name, info, output, do_output, verbose, browser_info)
   7.693 +                  loop(pending, running + (name -> (parent_result.heap, job)), results)
   7.694 +                }
   7.695 +                else {
   7.696 +                  progress.echo(name + " CANCELLED")
   7.697 +                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   7.698 +                }
   7.699 +              case None => sleep(); loop(pending, running, results)
   7.700 +            }
   7.701 +            ///}}}
   7.702 +          case None => sleep(); loop(pending, running, results)
   7.703 +        }
   7.704 +    }
   7.705 +
   7.706 +    val results =
   7.707 +      if (deps.is_empty) {
   7.708 +        progress.echo("### Nothing to build")
   7.709 +        Map.empty
   7.710 +      }
   7.711 +      else loop(queue, Map.empty, Map.empty)
   7.712 +
   7.713 +    val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
   7.714 +    if (rc != 0 && (verbose || !no_build)) {
   7.715 +      val unfinished =
   7.716 +        (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList
   7.717 +          .sorted(scala.math.Ordering.String)  // FIXME scala-2.10.0-RC1
   7.718 +      progress.echo("Unfinished session(s): " + commas(unfinished))
   7.719 +    }
   7.720 +    rc
   7.721 +  }
   7.722 +
   7.723 +
   7.724 +  /* command line entry point */
   7.725 +
   7.726 +  def main(args: Array[String])
   7.727 +  {
   7.728 +    Command_Line.tool {
   7.729 +      args.toList match {
   7.730 +        case
   7.731 +          Properties.Value.Boolean(requirements) ::
   7.732 +          Properties.Value.Boolean(all_sessions) ::
   7.733 +          Properties.Value.Boolean(build_heap) ::
   7.734 +          Properties.Value.Boolean(clean_build) ::
   7.735 +          Properties.Value.Int(max_jobs) ::
   7.736 +          Properties.Value.Boolean(list_files) ::
   7.737 +          Properties.Value.Boolean(no_build) ::
   7.738 +          Properties.Value.Boolean(system_mode) ::
   7.739 +          Properties.Value.Boolean(verbose) ::
   7.740 +          Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
   7.741 +            val options = (Options.init() /: build_options)(_ + _)
   7.742 +            val dirs =
   7.743 +              select_dirs.map(d => (true, Path.explode(d))) :::
   7.744 +              include_dirs.map(d => (false, Path.explode(d)))
   7.745 +            build(Build.Console_Progress, options, requirements, all_sessions, build_heap,
   7.746 +              clean_build, dirs, session_groups, max_jobs, list_files, no_build, system_mode,
   7.747 +              verbose, sessions)
   7.748 +        case _ => error("Bad arguments:\n" + cat_lines(args))
   7.749 +      }
   7.750 +    }
   7.751 +  }
   7.752 +}
   7.753 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/Tools/build_dialog.scala	Wed Jan 02 17:58:53 2013 +0100
     8.3 @@ -0,0 +1,135 @@
     8.4 +/*  Title:      Pure/Tools/build_dialog.scala
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +Dialog for session build process.
     8.8 +*/
     8.9 +
    8.10 +package isabelle
    8.11 +
    8.12 +
    8.13 +import java.awt.{GraphicsEnvironment, Point, Font}
    8.14 +
    8.15 +import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
    8.16 +  BorderPanel, MainFrame, TextArea, SwingApplication}
    8.17 +import scala.swing.event.ButtonClicked
    8.18 +
    8.19 +
    8.20 +object Build_Dialog
    8.21 +{
    8.22 +  def main(args: Array[String]) =
    8.23 +  {
    8.24 +    Platform.init_laf()
    8.25 +    try {
    8.26 +      args.toList match {
    8.27 +        case
    8.28 +          logic_option ::
    8.29 +          logic ::
    8.30 +          Properties.Value.Boolean(system_mode) ::
    8.31 +          include_dirs =>
    8.32 +            val more_dirs = include_dirs.map(s => ((false, Path.explode(s))))
    8.33 +
    8.34 +            val options = Options.init()
    8.35 +            val session =
    8.36 +              Isabelle_System.default_logic(logic,
    8.37 +                if (logic_option != "") options.string(logic_option) else "")
    8.38 +
    8.39 +            if (Build.build(Build.Ignore_Progress, options, build_heap = true, no_build = true,
    8.40 +                more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0)
    8.41 +            else
    8.42 +              Swing_Thread.later {
    8.43 +                val top = build_dialog(options, system_mode, more_dirs, session)
    8.44 +                top.pack()
    8.45 +
    8.46 +                val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
    8.47 +                top.location =
    8.48 +                  new Point(point.x - top.size.width / 2, point.y - top.size.height / 2)
    8.49 +
    8.50 +                top.visible = true
    8.51 +              }
    8.52 +        case _ => error("Bad arguments:\n" + cat_lines(args))
    8.53 +      }
    8.54 +    }
    8.55 +    catch {
    8.56 +      case exn: Throwable =>
    8.57 +        Library.error_dialog(null, "Isabelle build failure",
    8.58 +          Library.scrollable_text(Exn.message(exn)))
    8.59 +        sys.exit(2)
    8.60 +    }
    8.61 +  }
    8.62 +
    8.63 +
    8.64 +  def build_dialog(
    8.65 +    options: Options,
    8.66 +    system_mode: Boolean,
    8.67 +    more_dirs: List[(Boolean, Path)],
    8.68 +    session: String): MainFrame = new MainFrame
    8.69 +  {
    8.70 +    /* GUI state */
    8.71 +
    8.72 +    private var is_stopped = false
    8.73 +    private var return_code = 0
    8.74 +
    8.75 +
    8.76 +    /* text */
    8.77 +
    8.78 +    val text = new TextArea {
    8.79 +      font = new Font("SansSerif", Font.PLAIN, 14)
    8.80 +      editable = false
    8.81 +      columns = 40
    8.82 +      rows = 10
    8.83 +    }
    8.84 +
    8.85 +    val progress = new Build.Progress
    8.86 +    {
    8.87 +      override def echo(msg: String): Unit = Swing_Thread.now { text.append(msg + "\n") }
    8.88 +      override def stopped: Boolean =
    8.89 +        Swing_Thread.now { val b = is_stopped; is_stopped = false; b  }
    8.90 +    }
    8.91 +
    8.92 +
    8.93 +    /* action button */
    8.94 +
    8.95 +    var button_action: () => Unit = (() => is_stopped = true)
    8.96 +    val button = new Button("Cancel") {
    8.97 +      reactions += { case ButtonClicked(_) => button_action() }
    8.98 +    }
    8.99 +    def button_exit(rc: Int)
   8.100 +    {
   8.101 +      button.text = if (rc == 0) "OK" else "Exit"
   8.102 +      button_action = (() => sys.exit(rc))
   8.103 +      button.peer.getRootPane.setDefaultButton(button.peer)
   8.104 +    }
   8.105 +
   8.106 +    val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button)
   8.107 +
   8.108 +
   8.109 +    /* layout panel */
   8.110 +
   8.111 +    val layout_panel = new BorderPanel
   8.112 +    layout_panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
   8.113 +    layout_panel.layout(action_panel) = BorderPanel.Position.South
   8.114 +
   8.115 +    contents = layout_panel
   8.116 +
   8.117 +
   8.118 +    /* main build */
   8.119 +
   8.120 +    title = "Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")"
   8.121 +    progress.echo("Build started for Isabelle/" + session + " ...")
   8.122 +
   8.123 +    default_thread_pool.submit(() => {
   8.124 +      val (out, rc) =
   8.125 +        try {
   8.126 +          ("",
   8.127 +            Build.build(progress, options, build_heap = true, more_dirs = more_dirs,
   8.128 +              system_mode = system_mode, sessions = List(session)))
   8.129 +        }
   8.130 +        catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
   8.131 +      Swing_Thread.now {
   8.132 +        progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
   8.133 +        button_exit(rc)
   8.134 +      }
   8.135 +    })
   8.136 +  }
   8.137 +}
   8.138 +
     9.1 --- a/src/Pure/build-jars	Wed Jan 02 16:48:22 2013 +0100
     9.2 +++ b/src/Pure/build-jars	Wed Jan 02 17:58:53 2013 +0100
     9.3 @@ -39,8 +39,6 @@
     9.4    PIDE/text.scala
     9.5    PIDE/xml.scala
     9.6    PIDE/yxml.scala
     9.7 -  System/build.scala
     9.8 -  System/build_dialog.scala
     9.9    System/color_value.scala
    9.10    System/command_line.scala
    9.11    System/event_bus.scala
    9.12 @@ -64,6 +62,8 @@
    9.13    Thy/thy_info.scala
    9.14    Thy/thy_load.scala
    9.15    Thy/thy_syntax.scala
    9.16 +  Tools/build.scala
    9.17 +  Tools/build_dialog.scala
    9.18    library.scala
    9.19    package.scala
    9.20    term.scala