--- a/src/Pure/Tools/build_dialog.scala Wed Sep 11 10:57:09 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-/* Title: Pure/Tools/build_dialog.scala
- Author: Makarius
-
-Dialog for session build process.
-*/
-
-package isabelle
-
-
-import java.awt.{GraphicsEnvironment, Point, Font}
-
-import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
- BorderPanel, MainFrame, TextArea, SwingApplication, Component, Label}
-import scala.swing.event.ButtonClicked
-
-
-object Build_Dialog
-{
- /* command line entry point */
-
- def main(args: Array[String])
- {
- GUI.init_laf()
- try {
- args.toList match {
- case
- logic_option ::
- logic ::
- Properties.Value.Boolean(system_mode) ::
- include_dirs =>
- val options = Options.init()
- val dirs = include_dirs.map(Path.explode(_))
- val session =
- Isabelle_System.default_logic(logic,
- if (logic_option != "") options.string(logic_option) else "")
-
- val system_dialog = new System_Dialog
- dialog(options, system_dialog, system_mode, dirs, session)
- system_dialog.join_exit
-
- case _ => error("Bad arguments:\n" + cat_lines(args))
- }
- }
- catch {
- case exn: Throwable =>
- GUI.error_dialog(null, "Isabelle build failure", GUI.scrollable_text(Exn.message(exn)))
- sys.exit(2)
- }
- }
-
-
- /* dialog */
-
- def dialog(
- options: Options,
- system_dialog: System_Dialog,
- system_mode: Boolean,
- dirs: List[Path],
- session: String)
- {
- val more_dirs = dirs.map((false, _))
-
- if (Build.build(options = options, build_heap = true, no_build = true,
- more_dirs = more_dirs, sessions = List(session)) == 0)
- system_dialog.return_code(0)
- else {
- system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")")
- system_dialog.echo("Build started for Isabelle/" + session + " ...")
-
- val (out, rc) =
- try {
- ("",
- Build.build(options = options, progress = system_dialog,
- build_heap = true, more_dirs = more_dirs,
- system_mode = system_mode, sessions = List(session)))
- }
- catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
-
- system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
- system_dialog.return_code(rc)
- }
- }
-}
-