author | wenzelm |
Tue, 07 Apr 2020 21:49:36 +0200 | |
changeset 71726 | a5fda30edae2 |
parent 71725 | c255ed582095 |
child 71747 | 1dd514c8c1df |
permissions | -rw-r--r-- |
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 |
{ |
|
65256 | 24 |
def check_dialog(view: View) |
61288 | 25 |
{ |
65256 | 26 |
val options = PIDE.options.value |
71725
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
27 |
Isabelle_Thread.fork() { |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
28 |
try { |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
29 |
if (JEdit_Sessions.session_no_build || |
65256 | 30 |
JEdit_Sessions.session_build(options, no_build = true) == 0) |
71725
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
31 |
JEdit_Sessions.session_start(options) |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
32 |
else GUI_Thread.later { new Dialog(view) } |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
33 |
} |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
34 |
catch { |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
35 |
case exn: Throwable => |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
36 |
GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn))) |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
37 |
} |
61288 | 38 |
} |
39 |
} |
|
40 |
||
41 |
private class Dialog(view: View) extends JDialog(view) |
|
42 |
{ |
|
71601 | 43 |
val options: Options = PIDE.options.value |
65256 | 44 |
|
45 |
||
61288 | 46 |
/* text */ |
47 |
||
48 |
private val text = new TextArea { |
|
49 |
editable = false |
|
50 |
columns = 65 |
|
51 |
rows = 24 |
|
52 |
} |
|
61742
fd3b214b0979
clarified font: GUI defaults might change dynamically;
wenzelm
parents:
61680
diff
changeset
|
53 |
text.font = GUI.copy_font((new Label).font) |
61288 | 54 |
|
55 |
private val scroll_text = new ScrollPane(text) |
|
56 |
||
57 |
||
58 |
/* progress */ |
|
59 |
||
60 |
private val progress = new Progress { |
|
61 |
override def echo(txt: String): Unit = |
|
62 |
GUI_Thread.later { |
|
63 |
text.append(txt + "\n") |
|
64 |
val vertical = scroll_text.peer.getVerticalScrollBar |
|
65 |
vertical.setValue(vertical.getMaximum) |
|
66 |
} |
|
67 |
||
68957 | 68 |
override def theory(theory: Progress.Theory): Unit = echo(theory.message) |
61288 | 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 = |
|
71704 | 101 |
Delay.first(Time.seconds(1.0), gui = true) |
61288 | 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 |
{ |
|
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71725
diff
changeset
|
131 |
progress.stop |
61288 | 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 |
||
71692 | 164 |
Isabelle_Thread.fork(name = "session_build") { |
66973
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
65828
diff
changeset
|
165 |
progress.echo("Build started for Isabelle/" + PIDE.resources.session_name + " ...") |
61288 | 166 |
|
167 |
val (out, rc) = |
|
65256 | 168 |
try { ("", JEdit_Sessions.session_build(options, progress = progress)) } |
61288 | 169 |
catch { |
170 |
case exn: Throwable => |
|
65828 | 171 |
(Output.error_message_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2)) |
61288 | 172 |
} |
173 |
||
174 |
progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) |
|
61289 | 175 |
|
65256 | 176 |
if (rc == 0) JEdit_Sessions.session_start(options) |
61680 | 177 |
else progress.echo("Session build failed -- prover process remains inactive!") |
61288 | 178 |
|
179 |
return_code(rc) |
|
180 |
} |
|
181 |
} |
|
182 |
} |