author | wenzelm |
Wed, 02 Jan 2013 17:58:53 +0100 | |
changeset 50686 | d703e3aafa8c |
parent 50546 | src/Pure/System/build_dialog.scala@1b01a57d2749 |
child 50740 | 21098a577294 |
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, |
13 |
BorderPanel, MainFrame, TextArea, SwingApplication} |
|
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 |
{ |
50404
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
19 |
def main(args: Array[String]) = |
50365 | 20 |
{ |
50539 | 21 |
Platform.init_laf() |
50365 | 22 |
try { |
23 |
args.toList match { |
|
50369 | 24 |
case |
50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50381
diff
changeset
|
25 |
logic_option :: |
50546 | 26 |
logic :: |
50369 | 27 |
Properties.Value.Boolean(system_mode) :: |
50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50381
diff
changeset
|
28 |
include_dirs => |
50405
366c4a602500
clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents:
50404
diff
changeset
|
29 |
val more_dirs = include_dirs.map(s => ((false, Path.explode(s)))) |
50404
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
30 |
|
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
31 |
val options = Options.init() |
50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50381
diff
changeset
|
32 |
val session = |
50404
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
33 |
Isabelle_System.default_logic(logic, |
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
34 |
if (logic_option != "") options.string(logic_option) else "") |
50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50381
diff
changeset
|
35 |
|
50532
345b25cf2e4f
actually request heap image in initial up-to-date check;
wenzelm
parents:
50405
diff
changeset
|
36 |
if (Build.build(Build.Ignore_Progress, options, build_heap = true, no_build = true, |
50405
366c4a602500
clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents:
50404
diff
changeset
|
37 |
more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0) |
50404
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
38 |
else |
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
39 |
Swing_Thread.later { |
50405
366c4a602500
clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents:
50404
diff
changeset
|
40 |
val top = build_dialog(options, system_mode, more_dirs, session) |
50404
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
41 |
top.pack() |
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
42 |
|
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
43 |
val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint() |
50532
345b25cf2e4f
actually request heap image in initial up-to-date check;
wenzelm
parents:
50405
diff
changeset
|
44 |
top.location = |
345b25cf2e4f
actually request heap image in initial up-to-date check;
wenzelm
parents:
50405
diff
changeset
|
45 |
new Point(point.x - top.size.width / 2, point.y - top.size.height / 2) |
50404
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
46 |
|
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
47 |
top.visible = true |
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
48 |
} |
50365 | 49 |
case _ => error("Bad arguments:\n" + cat_lines(args)) |
50 |
} |
|
51 |
} |
|
52 |
catch { |
|
53 |
case exn: Throwable => |
|
54 |
Library.error_dialog(null, "Isabelle build failure", |
|
55 |
Library.scrollable_text(Exn.message(exn))) |
|
56 |
sys.exit(2) |
|
57 |
} |
|
58 |
} |
|
59 |
||
60 |
||
50369 | 61 |
def build_dialog( |
50404
898cac1dad5e
avoid startup within GUI thread -- it is only required later for dialog;
wenzelm
parents:
50403
diff
changeset
|
62 |
options: Options, |
50369 | 63 |
system_mode: Boolean, |
50405
366c4a602500
clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents:
50404
diff
changeset
|
64 |
more_dirs: List[(Boolean, Path)], |
50369 | 65 |
session: String): MainFrame = new MainFrame |
50365 | 66 |
{ |
50368 | 67 |
/* GUI state */ |
50365 | 68 |
|
50368 | 69 |
private var is_stopped = false |
70 |
private var return_code = 0 |
|
71 |
||
72 |
||
50365 | 73 |
/* text */ |
74 |
||
75 |
val text = new TextArea { |
|
50378 | 76 |
font = new Font("SansSerif", Font.PLAIN, 14) |
50365 | 77 |
editable = false |
50369 | 78 |
columns = 40 |
79 |
rows = 10 |
|
50365 | 80 |
} |
81 |
||
50368 | 82 |
val progress = new Build.Progress |
83 |
{ |
|
84 |
override def echo(msg: String): Unit = Swing_Thread.now { text.append(msg + "\n") } |
|
85 |
override def stopped: Boolean = |
|
86 |
Swing_Thread.now { val b = is_stopped; is_stopped = false; b } |
|
87 |
} |
|
88 |
||
50365 | 89 |
|
50376 | 90 |
/* action button */ |
50365 | 91 |
|
50376 | 92 |
var button_action: () => Unit = (() => is_stopped = true) |
93 |
val button = new Button("Cancel") { |
|
94 |
reactions += { case ButtonClicked(_) => button_action() } |
|
95 |
} |
|
96 |
def button_exit(rc: Int) |
|
97 |
{ |
|
98 |
button.text = if (rc == 0) "OK" else "Exit" |
|
99 |
button_action = (() => sys.exit(rc)) |
|
50381
d9711842f1f9
clarified default button (cf. org/gjt/sp/jedit/gui/OptionsDialog.java);
wenzelm
parents:
50379
diff
changeset
|
100 |
button.peer.getRootPane.setDefaultButton(button.peer) |
50365 | 101 |
} |
102 |
||
50376 | 103 |
val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button) |
50368 | 104 |
|
105 |
||
106 |
/* layout panel */ |
|
107 |
||
108 |
val layout_panel = new BorderPanel |
|
109 |
layout_panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center |
|
50376 | 110 |
layout_panel.layout(action_panel) = BorderPanel.Position.South |
50368 | 111 |
|
112 |
contents = layout_panel |
|
50369 | 113 |
|
114 |
||
115 |
/* main build */ |
|
116 |
||
50374 | 117 |
title = "Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")" |
50372 | 118 |
progress.echo("Build started for Isabelle/" + session + " ...") |
50369 | 119 |
|
120 |
default_thread_pool.submit(() => { |
|
121 |
val (out, rc) = |
|
122 |
try { |
|
123 |
("", |
|
50405
366c4a602500
clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents:
50404
diff
changeset
|
124 |
Build.build(progress, options, build_heap = true, more_dirs = more_dirs, |
50370 | 125 |
system_mode = system_mode, sessions = List(session))) |
50369 | 126 |
} |
127 |
catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } |
|
50376 | 128 |
Swing_Thread.now { |
129 |
progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) |
|
130 |
button_exit(rc) |
|
50371 | 131 |
} |
50369 | 132 |
}) |
50365 | 133 |
} |
134 |
} |
|
135 |