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.event.{WindowEvent, WindowAdapter} |
|
11 import javax.swing.{WindowConstants, JFrame, JDialog} |
|
12 |
|
13 import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel, |
|
14 BorderPanel, Frame, TextArea, Component, Label} |
|
15 import scala.swing.event.ButtonClicked |
|
16 |
|
17 |
|
18 class System_Dialog(owner: JFrame = null) extends Progress |
|
19 { |
|
20 /* component state -- owned by GUI thread */ |
|
21 |
|
22 private var _title = "Isabelle" |
|
23 private var _window: Option[Window] = None |
|
24 private var _return_code: Option[Int] = None |
|
25 |
|
26 private def check_window(): Window = |
|
27 { |
|
28 GUI_Thread.require {} |
|
29 |
|
30 _window match { |
|
31 case Some(window) => window |
|
32 case None => |
|
33 val window = new Window |
|
34 _window = Some(window) |
|
35 |
|
36 window.pack() |
|
37 window.setLocationRelativeTo(owner) |
|
38 window.setVisible(true) |
|
39 |
|
40 window |
|
41 } |
|
42 } |
|
43 |
|
44 private val result = Future.promise[Int] |
|
45 |
|
46 private def conclude() |
|
47 { |
|
48 GUI_Thread.require {} |
|
49 require(_return_code.isDefined) |
|
50 |
|
51 _window match { |
|
52 case None => |
|
53 case Some(window) => |
|
54 window.setVisible(false) |
|
55 window.dispose |
|
56 _window = None |
|
57 } |
|
58 |
|
59 try { result.fulfill(_return_code.get) } |
|
60 catch { case ERROR(_) => } |
|
61 } |
|
62 |
|
63 def join(): Int = result.join |
|
64 def join_exit(): Nothing = sys.exit(join) |
|
65 |
|
66 |
|
67 /* window */ |
|
68 |
|
69 private class Window extends JDialog(owner, _title) |
|
70 { |
|
71 setIconImages(GUI.isabelle_images()) |
|
72 |
|
73 |
|
74 /* text */ |
|
75 |
|
76 val text = new TextArea { |
|
77 editable = false |
|
78 columns = 65 |
|
79 rows = 24 |
|
80 } |
|
81 text.font = (new Label).font |
|
82 |
|
83 val scroll_text = new ScrollPane(text) |
|
84 |
|
85 |
|
86 /* layout panel with dynamic actions */ |
|
87 |
|
88 val action_panel = new FlowPanel(FlowPanel.Alignment.Center)() |
|
89 val layout_panel = new BorderPanel |
|
90 layout_panel.layout(scroll_text) = BorderPanel.Position.Center |
|
91 layout_panel.layout(action_panel) = BorderPanel.Position.South |
|
92 |
|
93 setContentPane(layout_panel.peer) |
|
94 |
|
95 def set_actions(cs: Component*) |
|
96 { |
|
97 action_panel.contents.clear |
|
98 action_panel.contents ++= cs |
|
99 layout_panel.revalidate |
|
100 layout_panel.repaint |
|
101 } |
|
102 |
|
103 |
|
104 /* close */ |
|
105 |
|
106 setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE) |
|
107 |
|
108 addWindowListener(new WindowAdapter { |
|
109 override def windowClosing(e: WindowEvent) { |
|
110 if (_return_code.isDefined) conclude() |
|
111 else stopping() |
|
112 } |
|
113 }) |
|
114 |
|
115 def stopping() |
|
116 { |
|
117 is_stopped = true |
|
118 set_actions(new Label("Stopping ...")) |
|
119 } |
|
120 |
|
121 val stop_button = new Button("Stop") { |
|
122 reactions += { case ButtonClicked(_) => stopping() } |
|
123 } |
|
124 |
|
125 var do_auto_close = true |
|
126 def can_auto_close: Boolean = do_auto_close && _return_code == Some(0) |
|
127 |
|
128 val auto_close = new CheckBox("Auto close") { |
|
129 reactions += { |
|
130 case ButtonClicked(_) => do_auto_close = this.selected |
|
131 if (can_auto_close) conclude() |
|
132 } |
|
133 } |
|
134 auto_close.selected = do_auto_close |
|
135 auto_close.tooltip = "Automatically close dialog when finished" |
|
136 |
|
137 set_actions(stop_button, auto_close) |
|
138 |
|
139 |
|
140 /* exit */ |
|
141 |
|
142 val delay_exit = |
|
143 GUI_Thread.delay_first(Time.seconds(1.0)) |
|
144 { |
|
145 if (can_auto_close) conclude() |
|
146 else { |
|
147 val button = |
|
148 new Button(if (_return_code == Some(0)) "OK" else "Exit") { |
|
149 reactions += { case ButtonClicked(_) => conclude() } |
|
150 } |
|
151 set_actions(button) |
|
152 button.peer.getRootPane.setDefaultButton(button.peer) |
|
153 } |
|
154 } |
|
155 } |
|
156 |
|
157 |
|
158 /* progress operations */ |
|
159 |
|
160 def title(txt: String): Unit = |
|
161 GUI_Thread.later { |
|
162 _title = txt |
|
163 _window.foreach(window => window.setTitle(txt)) |
|
164 } |
|
165 |
|
166 def return_code(rc: Int): Unit = |
|
167 GUI_Thread.later { |
|
168 _return_code = Some(rc) |
|
169 _window match { |
|
170 case None => conclude() |
|
171 case Some(window) => window.delay_exit.invoke |
|
172 } |
|
173 } |
|
174 |
|
175 override def echo(txt: String): Unit = |
|
176 GUI_Thread.later { |
|
177 val window = check_window() |
|
178 window.text.append(txt + "\n") |
|
179 val vertical = window.scroll_text.peer.getVerticalScrollBar |
|
180 vertical.setValue(vertical.getMaximum) |
|
181 } |
|
182 |
|
183 override def theory(session: String, theory: String): Unit = |
|
184 echo(session + ": theory " + theory) |
|
185 |
|
186 @volatile private var is_stopped = false |
|
187 override def stopped: Boolean = is_stopped |
|
188 } |
|