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