author | wenzelm |
Sat, 07 Sep 2013 17:23:05 +0200 | |
changeset 53460 | 6015a663b889 |
parent 53456 | d12be8f62285 |
permissions | -rw-r--r-- |
50686 | 1 |
/* Title: Pure/Tools/build_dialog.scala |
50365 | 2 |
Author: Makarius |
3 |
||
4 |
Dialog for session build process. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
50378 | 10 |
import java.awt.{GraphicsEnvironment, Point, Font} |
50379
a8b0d3729a69
added keyboard shortcut for button (canonical way to do that?);
wenzelm
parents:
50378
diff
changeset
|
11 |
|
50365 | 12 |
import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel, |
51254
5bae6fc0e125
more explicit GUI components for dynamic actions;
wenzelm
parents:
51253
diff
changeset
|
13 |
BorderPanel, MainFrame, TextArea, SwingApplication, Component, Label} |
50365 | 14 |
import scala.swing.event.ButtonClicked |
15 |
||
16 |
||
50404
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
17 |
object Build_Dialog |
50365 | 18 |
{ |
53449 | 19 |
/* command line entry point */ |
20 |
||
53456 | 21 |
def main(args: Array[String]) |
50365 | 22 |
{ |
51617 | 23 |
GUI.init_laf() |
50365 | 24 |
try { |
25 |
args.toList match { |
|
50369 | 26 |
case |
50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50381
diff
changeset
|
27 |
logic_option :: |
50546 | 28 |
logic :: |
50369 | 29 |
Properties.Value.Boolean(system_mode) :: |
50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50381
diff
changeset
|
30 |
include_dirs => |
50404
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
31 |
val options = Options.init() |
53449 | 32 |
val dirs = include_dirs.map(Path.explode(_)) |
50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50381
diff
changeset
|
33 |
val session = |
50404
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
34 |
Isabelle_System.default_logic(logic, |
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
35 |
if (logic_option != "") options.string(logic_option) else "") |
50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50381
diff
changeset
|
36 |
|
53456 | 37 |
val system_dialog = new System_Dialog |
38 |
dialog(options, system_dialog, system_mode, dirs, session) |
|
53460 | 39 |
system_dialog.join_exit |
50404
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
40 |
|
50365 | 41 |
case _ => error("Bad arguments:\n" + cat_lines(args)) |
42 |
} |
|
43 |
} |
|
44 |
catch { |
|
45 |
case exn: Throwable => |
|
51616 | 46 |
GUI.error_dialog(null, "Isabelle build failure", GUI.scrollable_text(Exn.message(exn))) |
50365 | 47 |
sys.exit(2) |
48 |
} |
|
49 |
} |
|
50 |
||
51 |
||
53449 | 52 |
/* dialog */ |
53 |
||
53456 | 54 |
def dialog( |
55 |
options: Options, |
|
56 |
system_dialog: System_Dialog, |
|
57 |
system_mode: Boolean, |
|
58 |
dirs: List[Path], |
|
59 |
session: String) |
|
53449 | 60 |
{ |
61 |
val more_dirs = dirs.map((false, _)) |
|
62 |
||
63 |
if (Build.build(options = options, build_heap = true, no_build = true, |
|
53456 | 64 |
more_dirs = more_dirs, sessions = List(session)) == 0) |
65 |
system_dialog.return_code(0) |
|
53449 | 66 |
else { |
53456 | 67 |
system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")") |
68 |
system_dialog.echo("Build started for Isabelle/" + session + " ...") |
|
51254
5bae6fc0e125
more explicit GUI components for dynamic actions;
wenzelm
parents:
51253
diff
changeset
|
69 |
|
50369 | 70 |
val (out, rc) = |
71 |
try { |
|
72 |
("", |
|
53456 | 73 |
Build.build(options = options, progress = system_dialog, |
52115 | 74 |
build_heap = true, more_dirs = more_dirs, |
50370 | 75 |
system_mode = system_mode, sessions = List(session))) |
50369 | 76 |
} |
77 |
catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } |
|
53456 | 78 |
|
79 |
system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) |
|
80 |
system_dialog.return_code(rc) |
|
81 |
} |
|
50365 | 82 |
} |
83 |
} |
|
84 |