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