author | wenzelm |
Sat, 07 Sep 2013 14:14:25 +0200 | |
changeset 53455 | e9a3390217b3 |
parent 53454 | 1a0c39c728a1 |
child 53456 | d12be8f62285 |
permissions | -rw-r--r-- |
53453
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Tools/system_dialog.scala |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
3 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
4 |
Dialog for system processes, with optional output window. |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
6 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
8 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
9 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
10 |
import java.awt.{GraphicsEnvironment, Point, Font} |
53455 | 11 |
import javax.swing.WindowConstants |
53453
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
12 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
13 |
import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel, |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
14 |
BorderPanel, Frame, TextArea, SwingApplication, Component, Label} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
15 |
import scala.swing.event.ButtonClicked |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
16 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
17 |
|
53454 | 18 |
class System_Dialog extends Build.Progress |
53453
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
19 |
{ |
53454 | 20 |
val result = Future.promise[Int] |
21 |
||
22 |
||
53453
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
23 |
/* GUI state -- owned by Swing thread */ |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
24 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
25 |
private var _title = "Isabelle" |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
26 |
private var _window: Option[Window] = None |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
27 |
private var _return_code: Option[Int] = None |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
28 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
29 |
private def check_window(): Window = |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
30 |
{ |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
31 |
Swing_Thread.require() |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
32 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
33 |
_window match { |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
34 |
case Some(window) => window |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
35 |
case None => |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
36 |
val window = new Window |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
37 |
_window = Some(window) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
38 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
39 |
window.pack() |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
40 |
val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint() |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
41 |
window.location = |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
42 |
new Point(point.x - window.size.width / 2, point.y - window.size.height / 2) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
43 |
window.visible = true |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
44 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
45 |
window |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
46 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
47 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
48 |
|
53454 | 49 |
private def conclude() |
53453
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
50 |
{ |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
51 |
Swing_Thread.require() |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
52 |
require(_return_code.isDefined) |
53454 | 53 |
require(!result.is_finished) |
53453
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
54 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
55 |
_window match { |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
56 |
case None => |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
57 |
case Some(window) => |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
58 |
window.visible = false |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
59 |
_window = None |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
60 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
61 |
|
53454 | 62 |
result.fulfill(_return_code.get) |
53453
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
63 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
64 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
65 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
66 |
/* window */ |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
67 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
68 |
private class Window extends Frame |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
69 |
{ |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
70 |
title = _title |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
71 |
iconImage = GUI.isabelle_image() |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
72 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
73 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
74 |
/* text */ |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
75 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
76 |
val text = new TextArea { |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
77 |
font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
78 |
editable = false |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
79 |
columns = 50 |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
80 |
rows = 20 |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
81 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
82 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
83 |
val scroll_text = new ScrollPane(text) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
84 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
85 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
86 |
/* layout panel with dynamic actions */ |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
87 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
88 |
val action_panel = new FlowPanel(FlowPanel.Alignment.Center)() |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
89 |
val layout_panel = new BorderPanel |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
90 |
layout_panel.layout(scroll_text) = BorderPanel.Position.Center |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
91 |
layout_panel.layout(action_panel) = BorderPanel.Position.South |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
92 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
93 |
contents = layout_panel |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
94 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
95 |
def set_actions(cs: Component*) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
96 |
{ |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
97 |
action_panel.contents.clear |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
98 |
action_panel.contents ++= cs |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
99 |
layout_panel.revalidate |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
100 |
layout_panel.repaint |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
101 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
102 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
103 |
|
53455 | 104 |
/* close */ |
105 |
||
106 |
peer.setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE) |
|
107 |
||
108 |
override def closeOperation { |
|
109 |
if (_return_code.isDefined) conclude() |
|
110 |
else stopping() |
|
111 |
} |
|
112 |
||
113 |
def stopping() |
|
114 |
{ |
|
115 |
is_stopped = true |
|
116 |
set_actions(new Label("Stopping ...")) |
|
117 |
} |
|
118 |
||
119 |
val stop_button = new Button("Stop") { |
|
120 |
reactions += { case ButtonClicked(_) => stopping() } |
|
121 |
} |
|
53453
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
122 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
123 |
var do_auto_close = true |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
124 |
def can_auto_close: Boolean = do_auto_close && _return_code == Some(0) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
125 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
126 |
val auto_close = new CheckBox("Auto close") { |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
127 |
reactions += { |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
128 |
case ButtonClicked(_) => do_auto_close = this.selected |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
129 |
if (can_auto_close) conclude() |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
130 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
131 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
132 |
auto_close.selected = do_auto_close |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
133 |
auto_close.tooltip = "Automatically close dialog when finished" |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
134 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
135 |
set_actions(stop_button, auto_close) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
136 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
137 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
138 |
/* exit */ |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
139 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
140 |
val delay_exit = |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
141 |
Swing_Thread.delay_first(Time.seconds(1.0)) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
142 |
{ |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
143 |
if (can_auto_close) conclude() |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
144 |
else { |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
145 |
val button = |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
146 |
new Button(if (_return_code == Some(0)) "OK" else "Exit") { |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
147 |
reactions += { case ButtonClicked(_) => conclude() } |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
148 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
149 |
set_actions(button) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
150 |
button.peer.getRootPane.setDefaultButton(button.peer) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
151 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
152 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
153 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
154 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
155 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
156 |
/* progress operations */ |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
157 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
158 |
def title(txt: String): Unit = |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
159 |
Swing_Thread.later { |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
160 |
_title = txt |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
161 |
_window.foreach(window => window.title = txt) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
162 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
163 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
164 |
def return_code(rc: Int): Unit = |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
165 |
Swing_Thread.later { |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
166 |
_return_code = Some(rc) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
167 |
_window.foreach(window => window.delay_exit.invoke) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
168 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
169 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
170 |
override def echo(txt: String): Unit = |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
171 |
Swing_Thread.later { |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
172 |
val window = check_window() |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
173 |
window.text.append(txt + "\n") |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
174 |
val vertical = window.scroll_text.peer.getVerticalScrollBar |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
175 |
vertical.setValue(vertical.getMaximum) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
176 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
177 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
178 |
override def theory(session: String, theory: String): Unit = |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
179 |
echo(session + ": theory " + theory) |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
180 |
|
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
181 |
@volatile private var is_stopped = false |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
182 |
override def stopped: Boolean = is_stopped |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
183 |
} |
20ff79162ff3
dialog for system processes, with optional output window;
wenzelm
parents:
diff
changeset
|
184 |