61288
|
1 |
/* Title: Tools/jEdit/src/session_build.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Session build management.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle.jedit
|
|
8 |
|
|
9 |
|
|
10 |
import isabelle._
|
|
11 |
|
|
12 |
import java.awt.event.{WindowEvent, WindowAdapter}
|
|
13 |
import javax.swing.{WindowConstants, JDialog}
|
|
14 |
|
|
15 |
import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
|
|
16 |
BorderPanel, TextArea, Component, Label}
|
|
17 |
import scala.swing.event.ButtonClicked
|
|
18 |
|
|
19 |
import org.gjt.sp.jedit.View
|
|
20 |
|
|
21 |
|
|
22 |
object Session_Build
|
|
23 |
{
|
|
24 |
def session_build(view: View)
|
|
25 |
{
|
|
26 |
GUI_Thread.require {}
|
|
27 |
|
|
28 |
try {
|
|
29 |
if (Isabelle_Logic.session_build_mode() == "none" ||
|
|
30 |
Isabelle_Logic.session_build(no_build = true) == 0) Isabelle_Logic.session_start()
|
|
31 |
else new Dialog(view)
|
|
32 |
}
|
|
33 |
catch {
|
|
34 |
case exn: Throwable =>
|
|
35 |
GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
|
|
36 |
}
|
|
37 |
}
|
|
38 |
|
|
39 |
private class Dialog(view: View) extends JDialog(view)
|
|
40 |
{
|
|
41 |
/* text */
|
|
42 |
|
|
43 |
private val text = new TextArea {
|
|
44 |
editable = false
|
|
45 |
columns = 65
|
|
46 |
rows = 24
|
|
47 |
}
|
|
48 |
text.font = (new Label).font
|
|
49 |
|
|
50 |
private val scroll_text = new ScrollPane(text)
|
|
51 |
|
|
52 |
|
|
53 |
/* progress */
|
|
54 |
|
|
55 |
@volatile private var is_stopped = false
|
|
56 |
|
|
57 |
private val progress = new Progress {
|
|
58 |
override def echo(txt: String): Unit =
|
|
59 |
GUI_Thread.later {
|
|
60 |
text.append(txt + "\n")
|
|
61 |
val vertical = scroll_text.peer.getVerticalScrollBar
|
|
62 |
vertical.setValue(vertical.getMaximum)
|
|
63 |
}
|
|
64 |
|
|
65 |
override def theory(session: String, theory: String): Unit =
|
|
66 |
echo(session + ": theory " + theory)
|
|
67 |
|
|
68 |
override def stopped: Boolean = is_stopped
|
|
69 |
}
|
|
70 |
|
|
71 |
|
|
72 |
/* layout panel with dynamic actions */
|
|
73 |
|
|
74 |
private val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
|
|
75 |
private val layout_panel = new BorderPanel
|
|
76 |
layout_panel.layout(scroll_text) = BorderPanel.Position.Center
|
|
77 |
layout_panel.layout(action_panel) = BorderPanel.Position.South
|
|
78 |
|
|
79 |
setContentPane(layout_panel.peer)
|
|
80 |
|
|
81 |
private def set_actions(cs: Component*)
|
|
82 |
{
|
|
83 |
action_panel.contents.clear
|
|
84 |
action_panel.contents ++= cs
|
|
85 |
layout_panel.revalidate
|
|
86 |
layout_panel.repaint
|
|
87 |
}
|
|
88 |
|
|
89 |
|
|
90 |
/* return code and exit */
|
|
91 |
|
|
92 |
private var _return_code: Option[Int] = None
|
|
93 |
|
|
94 |
private def return_code(rc: Int): Unit =
|
|
95 |
GUI_Thread.later {
|
|
96 |
_return_code = Some(rc)
|
|
97 |
delay_exit.invoke
|
|
98 |
}
|
|
99 |
|
|
100 |
private val delay_exit =
|
|
101 |
GUI_Thread.delay_first(Time.seconds(1.0))
|
|
102 |
{
|
|
103 |
if (can_auto_close) conclude()
|
|
104 |
else {
|
61299
|
105 |
val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } }
|
61288
|
106 |
set_actions(button)
|
|
107 |
button.peer.getRootPane.setDefaultButton(button.peer)
|
|
108 |
}
|
|
109 |
}
|
|
110 |
|
|
111 |
private def conclude()
|
|
112 |
{
|
|
113 |
setVisible(false)
|
|
114 |
dispose()
|
|
115 |
}
|
|
116 |
|
|
117 |
|
|
118 |
/* close */
|
|
119 |
|
|
120 |
setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
|
|
121 |
|
|
122 |
addWindowListener(new WindowAdapter {
|
|
123 |
override def windowClosing(e: WindowEvent) {
|
|
124 |
if (_return_code.isDefined) conclude()
|
|
125 |
else stopping()
|
|
126 |
}
|
|
127 |
})
|
|
128 |
|
|
129 |
private def stopping()
|
|
130 |
{
|
|
131 |
is_stopped = true
|
|
132 |
set_actions(new Label("Stopping ..."))
|
|
133 |
}
|
|
134 |
|
|
135 |
private val stop_button = new Button("Stop") {
|
|
136 |
reactions += { case ButtonClicked(_) => stopping() }
|
|
137 |
}
|
|
138 |
|
|
139 |
private var do_auto_close = true
|
|
140 |
private def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
|
|
141 |
|
|
142 |
private val auto_close = new CheckBox("Auto close") {
|
|
143 |
reactions += {
|
|
144 |
case ButtonClicked(_) => do_auto_close = this.selected
|
|
145 |
if (can_auto_close) conclude()
|
|
146 |
}
|
|
147 |
}
|
|
148 |
auto_close.selected = do_auto_close
|
|
149 |
auto_close.tooltip = "Automatically close dialog when finished"
|
|
150 |
|
|
151 |
set_actions(stop_button, auto_close)
|
|
152 |
|
|
153 |
|
|
154 |
/* main */
|
|
155 |
|
|
156 |
setTitle("Isabelle build (" +
|
|
157 |
Isabelle_System.getenv("ML_IDENTIFIER") + " / " +
|
|
158 |
"jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")")
|
|
159 |
|
|
160 |
pack()
|
|
161 |
setLocationRelativeTo(view)
|
|
162 |
setVisible(true)
|
|
163 |
|
61556
|
164 |
Standard_Thread.fork("session_build") {
|
61288
|
165 |
progress.echo("Build started for Isabelle/" + Isabelle_Logic.session_name() + " ...")
|
|
166 |
|
|
167 |
val (out, rc) =
|
|
168 |
try { ("", Isabelle_Logic.session_build(progress = progress)) }
|
|
169 |
catch {
|
|
170 |
case exn: Throwable =>
|
|
171 |
(Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
|
|
172 |
}
|
|
173 |
|
|
174 |
progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
|
61289
|
175 |
|
61288
|
176 |
if (rc == 0) Isabelle_Logic.session_start()
|
61680
|
177 |
else progress.echo("Session build failed -- prover process remains inactive!")
|
61288
|
178 |
|
|
179 |
return_code(rc)
|
|
180 |
}
|
|
181 |
}
|
|
182 |
}
|