author | paulson <lp15@cam.ac.uk> |
Wed, 24 Apr 2024 20:56:26 +0100 | |
changeset 80149 | 40a3fc07a587 |
parent 79052 | d5cf21ad8b47 |
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 |
||
75853 | 15 |
import scala.swing.{ScrollPane, FlowPanel, BorderPanel, TextArea, Component, Label} |
61288 | 16 |
|
17 |
import org.gjt.sp.jedit.View |
|
18 |
||
19 |
||
75393 | 20 |
object Session_Build { |
21 |
def check_dialog(view: View): Unit = { |
|
65256 | 22 |
val options = PIDE.options.value |
71725
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
23 |
Isabelle_Thread.fork() { |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
24 |
try { |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
25 |
if (JEdit_Sessions.session_no_build || |
65256 | 26 |
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
|
27 |
JEdit_Sessions.session_start(options) |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
28 |
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
|
29 |
} |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
30 |
catch { |
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
31 |
case exn: Throwable => |
76344
adb3f8d33838
more informative errors, with optional exception trace as in Command_Line.tool;
wenzelm
parents:
75854
diff
changeset
|
32 |
GUI.dialog(view, "Isabelle build", GUI.scrollable_text(Exn.print(exn))) |
71725
c255ed582095
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
wenzelm
parents:
71704
diff
changeset
|
33 |
} |
61288 | 34 |
} |
35 |
} |
|
36 |
||
75393 | 37 |
private class Dialog(view: View) extends JDialog(view) { |
71601 | 38 |
val options: Options = PIDE.options.value |
65256 | 39 |
|
40 |
||
61288 | 41 |
/* text */ |
42 |
||
79051 | 43 |
private val text = new TextArea |
44 |
text.editable = false |
|
45 |
text.columns = 60 |
|
46 |
text.rows = 24 |
|
61742
fd3b214b0979
clarified font: GUI defaults might change dynamically;
wenzelm
parents:
61680
diff
changeset
|
47 |
text.font = GUI.copy_font((new Label).font) |
79052
d5cf21ad8b47
workaround for "fix" JDK-4512626 in Java 20/21: avoid spurious caret in read-only text;
wenzelm
parents:
79051
diff
changeset
|
48 |
text.caret.color = text.background |
61288 | 49 |
|
50 |
private val scroll_text = new ScrollPane(text) |
|
51 |
||
52 |
||
53 |
/* progress */ |
|
54 |
||
55 |
private val progress = new Progress { |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77502
diff
changeset
|
56 |
override def output(message: Progress.Message): Unit = |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77502
diff
changeset
|
57 |
if (do_output(message)) { |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77502
diff
changeset
|
58 |
GUI_Thread.later { |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77502
diff
changeset
|
59 |
text.append(message.output_text + "\n") |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77502
diff
changeset
|
60 |
val vertical = scroll_text.peer.getVerticalScrollBar |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77502
diff
changeset
|
61 |
vertical.setValue(vertical.getMaximum) |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77502
diff
changeset
|
62 |
} |
61288 | 63 |
} |
77532 | 64 |
|
65 |
override def theory(theory: Progress.Theory): Unit = |
|
66 |
output(theory.message.copy(verbose = false)) |
|
61288 | 67 |
} |
68 |
||
69 |
||
70 |
/* layout panel with dynamic actions */ |
|
71 |
||
72 |
private val action_panel = new FlowPanel(FlowPanel.Alignment.Center)() |
|
73 |
private val layout_panel = new BorderPanel |
|
74 |
layout_panel.layout(scroll_text) = BorderPanel.Position.Center |
|
75 |
layout_panel.layout(action_panel) = BorderPanel.Position.South |
|
76 |
||
77 |
setContentPane(layout_panel.peer) |
|
78 |
||
75393 | 79 |
private def set_actions(cs: Component*): Unit = { |
73367 | 80 |
action_panel.contents.clear() |
61288 | 81 |
action_panel.contents ++= cs |
73367 | 82 |
layout_panel.revalidate() |
83 |
layout_panel.repaint() |
|
61288 | 84 |
} |
85 |
||
86 |
||
87 |
/* return code and exit */ |
|
88 |
||
89 |
private var _return_code: Option[Int] = None |
|
90 |
||
91 |
private def return_code(rc: Int): Unit = |
|
92 |
GUI_Thread.later { |
|
93 |
_return_code = Some(rc) |
|
73367 | 94 |
delay_exit.invoke() |
61288 | 95 |
} |
96 |
||
97 |
private val delay_exit = |
|
75393 | 98 |
Delay.first(Time.seconds(1.0), gui = true) { |
61288 | 99 |
if (can_auto_close) conclude() |
100 |
else { |
|
75853 | 101 |
val button = new GUI.Button("Close") { override def clicked(): Unit = conclude() } |
61288 | 102 |
set_actions(button) |
103 |
button.peer.getRootPane.setDefaultButton(button.peer) |
|
104 |
} |
|
105 |
} |
|
106 |
||
75393 | 107 |
private def conclude(): Unit = { |
61288 | 108 |
setVisible(false) |
109 |
dispose() |
|
110 |
} |
|
111 |
||
112 |
||
113 |
/* close */ |
|
114 |
||
115 |
setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE) |
|
116 |
||
117 |
addWindowListener(new WindowAdapter { |
|
75393 | 118 |
override def windowClosing(e: WindowEvent): Unit = { |
61288 | 119 |
if (_return_code.isDefined) conclude() |
120 |
else stopping() |
|
121 |
} |
|
122 |
}) |
|
123 |
||
75393 | 124 |
private def stopping(): Unit = { |
73367 | 125 |
progress.stop() |
61288 | 126 |
set_actions(new Label("Stopping ...")) |
127 |
} |
|
128 |
||
75853 | 129 |
private val stop_button = new GUI.Button("Stop") { |
130 |
override def clicked(): Unit = stopping() |
|
61288 | 131 |
} |
132 |
||
133 |
private var do_auto_close = true |
|
134 |
private def can_auto_close: Boolean = do_auto_close && _return_code == Some(0) |
|
135 |
||
75854 | 136 |
private val auto_close = new GUI.Check("Auto close", init = do_auto_close) { |
75852 | 137 |
tooltip = "Automatically close dialog when finished" |
138 |
override def clicked(state: Boolean): Unit = { |
|
139 |
do_auto_close = state |
|
61288 | 140 |
if (can_auto_close) conclude() |
141 |
} |
|
142 |
} |
|
143 |
||
144 |
set_actions(stop_button, auto_close) |
|
145 |
||
146 |
||
147 |
/* main */ |
|
148 |
||
77719 | 149 |
setTitle("Isabelle build (" + Isabelle_System.ml_identifier() + " / " + |
61288 | 150 |
"jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")") |
151 |
||
152 |
pack() |
|
153 |
setLocationRelativeTo(view) |
|
154 |
setVisible(true) |
|
155 |
||
71692 | 156 |
Isabelle_Thread.fork(name = "session_build") { |
75752 | 157 |
progress.echo("Build started for Isabelle/" + |
158 |
PIDE.resources.session_base.session_name + " ...") |
|
61288 | 159 |
|
160 |
val (out, rc) = |
|
65256 | 161 |
try { ("", JEdit_Sessions.session_build(options, progress = progress)) } |
61288 | 162 |
catch { |
163 |
case exn: Throwable => |
|
74068 | 164 |
(Output.error_message_text(Exn.message(exn)) + "\n", Exn.failure_rc(exn)) |
61288 | 165 |
} |
166 |
||
74306 | 167 |
val ok = rc == Process_Result.RC.ok |
168 |
progress.echo(out + (if (ok) "OK" else Process_Result.RC.print_long(rc)) + "\n") |
|
61289 | 169 |
|
74306 | 170 |
if (ok) JEdit_Sessions.session_start(options) |
61680 | 171 |
else progress.echo("Session build failed -- prover process remains inactive!") |
61288 | 172 |
|
173 |
return_code(rc) |
|
174 |
} |
|
175 |
} |
|
176 |
} |