author | wenzelm |
Sat, 12 Jan 2013 18:13:28 +0100 | |
changeset 50848 | 4e123d57c9b4 |
parent 50846 | 529e652d389d |
child 50850 | 4cd2d090be8f |
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 |
50742 | 70 |
private var return_code = 2 |
50368 | 71 |
|
50740 | 72 |
override def closeOperation { sys.exit(return_code) } |
73 |
||
50368 | 74 |
|
50365 | 75 |
/* text */ |
76 |
||
77 |
val text = new TextArea { |
|
50378 | 78 |
font = new Font("SansSerif", Font.PLAIN, 14) |
50365 | 79 |
editable = false |
50369 | 80 |
columns = 40 |
81 |
rows = 10 |
|
50365 | 82 |
} |
83 |
||
50368 | 84 |
val progress = new Build.Progress |
85 |
{ |
|
50846
529e652d389d
more uniform theory progress in build -v and build_dialog;
wenzelm
parents:
50845
diff
changeset
|
86 |
override def echo(msg: String): Unit = |
529e652d389d
more uniform theory progress in build -v and build_dialog;
wenzelm
parents:
50845
diff
changeset
|
87 |
Swing_Thread.later { text.append(msg + "\n") } |
529e652d389d
more uniform theory progress in build -v and build_dialog;
wenzelm
parents:
50845
diff
changeset
|
88 |
override def theory(session: String, theory: String): Unit = |
529e652d389d
more uniform theory progress in build -v and build_dialog;
wenzelm
parents:
50845
diff
changeset
|
89 |
echo(session + ": theory " + theory) |
50368 | 90 |
override def stopped: Boolean = |
91 |
Swing_Thread.now { val b = is_stopped; is_stopped = false; b } |
|
92 |
} |
|
93 |
||
50365 | 94 |
|
50848
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
95 |
/* action panel */ |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
96 |
|
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
97 |
var do_auto_close = true |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
98 |
def check_auto_close(): Unit = if (do_auto_close && return_code == 0) sys.exit(return_code) |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
99 |
|
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
100 |
val auto_close = new CheckBox("Auto close") { |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
101 |
reactions += { |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
102 |
case ButtonClicked(_) => do_auto_close = this.selected |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
103 |
check_auto_close() |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
104 |
} |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
105 |
} |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
106 |
auto_close.selected = do_auto_close |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
107 |
auto_close.tooltip = "Automatically close dialog when finished" |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
108 |
|
50365 | 109 |
|
50376 | 110 |
var button_action: () => Unit = (() => is_stopped = true) |
111 |
val button = new Button("Cancel") { |
|
112 |
reactions += { case ButtonClicked(_) => button_action() } |
|
113 |
} |
|
50848
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
114 |
def button_exit() |
50376 | 115 |
{ |
50848
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
116 |
check_auto_close() |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
117 |
button.text = if (return_code == 0) "OK" else "Exit" |
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
118 |
button_action = (() => sys.exit(return_code)) |
50381
d9711842f1f9
clarified default button (cf. org/gjt/sp/jedit/gui/OptionsDialog.java);
wenzelm
parents:
50379
diff
changeset
|
119 |
button.peer.getRootPane.setDefaultButton(button.peer) |
50365 | 120 |
} |
121 |
||
50848
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
122 |
|
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
123 |
val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button, auto_close) |
50368 | 124 |
|
125 |
||
126 |
/* layout panel */ |
|
127 |
||
128 |
val layout_panel = new BorderPanel |
|
129 |
layout_panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center |
|
50376 | 130 |
layout_panel.layout(action_panel) = BorderPanel.Position.South |
50368 | 131 |
|
132 |
contents = layout_panel |
|
50369 | 133 |
|
134 |
||
135 |
/* main build */ |
|
136 |
||
50374 | 137 |
title = "Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")" |
50372 | 138 |
progress.echo("Build started for Isabelle/" + session + " ...") |
50369 | 139 |
|
140 |
default_thread_pool.submit(() => { |
|
141 |
val (out, rc) = |
|
142 |
try { |
|
143 |
("", |
|
50405
366c4a602500
clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents:
50404
diff
changeset
|
144 |
Build.build(progress, options, build_heap = true, more_dirs = more_dirs, |
50370 | 145 |
system_mode = system_mode, sessions = List(session))) |
50369 | 146 |
} |
147 |
catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } |
|
50376 | 148 |
Swing_Thread.now { |
149 |
progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) |
|
50740 | 150 |
return_code = rc |
50848
4e123d57c9b4
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
wenzelm
parents:
50846
diff
changeset
|
151 |
button_exit() |
50371 | 152 |
} |
50369 | 153 |
}) |
50365 | 154 |
} |
155 |
} |
|
156 |