author | wenzelm |
Wed, 21 Dec 2022 13:22:57 +0100 | |
changeset 76727 | 6d95e8a636e2 |
parent 76726 | c83dfd565283 |
child 76732 | 0ba6f360d38a |
permissions | -rw-r--r-- |
75816 | 1 |
/* Title: Tools/jEdit/src/document_dockable.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Dockable window for document build support. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
import java.awt.BorderLayout |
|
13 |
import java.awt.event.{ComponentEvent, ComponentAdapter} |
|
14 |
||
76023 | 15 |
import scala.swing.{ScrollPane, TextArea, Label, TabbedPane, BorderPanel, Component} |
76602 | 16 |
import scala.swing.event.SelectionChanged |
76023 | 17 |
|
75816 | 18 |
import org.gjt.sp.jedit.{jEdit, View} |
19 |
||
20 |
||
76023 | 21 |
object Document_Dockable { |
76491 | 22 |
/* state */ |
23 |
||
76023 | 24 |
object Status extends Enumeration { |
25 |
val WAITING = Value("waiting") |
|
26 |
val RUNNING = Value("running") |
|
27 |
val FINISHED = Value("finished") |
|
28 |
} |
|
29 |
||
30 |
object State { |
|
76681 | 31 |
def init(): State = State() |
76023 | 32 |
} |
33 |
||
34 |
sealed case class State( |
|
76606 | 35 |
progress: Progress = new Progress, |
76023 | 36 |
process: Future[Unit] = Future.value(()), |
76681 | 37 |
status: Status.Value = Status.FINISHED, |
38 |
output: List[XML.Tree] = Nil |
|
39 |
) { |
|
40 |
def run(progress: Progress, process: Future[Unit]): State = |
|
41 |
copy(progress = progress, process = process, status = Status.RUNNING) |
|
42 |
||
76718 | 43 |
def finish(output: List[XML.Tree]): State = |
44 |
copy(process = Future.value(()), status = Status.FINISHED, output = output) |
|
45 |
||
46 |
def ok: Boolean = !output.exists(Protocol.is_error) |
|
76681 | 47 |
} |
76023 | 48 |
} |
49 |
||
75816 | 50 |
class Document_Dockable(view: View, position: String) extends Dockable(view, position) { |
76609
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
51 |
dockable => |
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
52 |
|
75816 | 53 |
GUI_Thread.require {} |
54 |
||
55 |
||
76023 | 56 |
/* component state -- owned by GUI thread */ |
57 |
||
76681 | 58 |
private val current_state = Synchronized(Document_Dockable.State.init()) |
76023 | 59 |
|
60 |
private val process_indicator = new Process_Indicator |
|
61 |
private val pretty_text_area = new Pretty_Text_Area(view) |
|
62 |
private val message_pane = new TabbedPane |
|
63 |
||
76034 | 64 |
private def show_state(): Unit = GUI_Thread.later { |
76023 | 65 |
val st = current_state.value |
66 |
||
67 |
pretty_text_area.update(Document.Snapshot.init, Command.Results.empty, st.output) |
|
75816 | 68 |
|
76023 | 69 |
st.status match { |
70 |
case Document_Dockable.Status.WAITING => |
|
71 |
process_indicator.update("Waiting for PIDE document content ...", 5) |
|
72 |
case Document_Dockable.Status.RUNNING => |
|
73 |
process_indicator.update("Running document build process ...", 15) |
|
74 |
case Document_Dockable.Status.FINISHED => |
|
75 |
process_indicator.update(null, 0) |
|
76 |
} |
|
76034 | 77 |
} |
76023 | 78 |
|
76034 | 79 |
private def show_page(page: TabbedPane.Page): Unit = GUI_Thread.later { |
80 |
message_pane.selection.page = page |
|
76023 | 81 |
} |
82 |
||
83 |
||
84 |
/* text area with zoom/resize */ |
|
75816 | 85 |
|
86 |
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation |
|
87 |
||
76021
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
88 |
private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
89 |
private def handle_resize(): Unit = GUI_Thread.require { pretty_text_area.zoom(zoom) } |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
90 |
|
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
91 |
private val delay_resize: Delay = |
76610 | 92 |
Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } |
76021
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
93 |
|
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
94 |
addComponentListener(new ComponentAdapter { |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
95 |
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
96 |
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
97 |
}) |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
98 |
|
76023 | 99 |
|
100 |
/* progress log */ |
|
101 |
||
76489
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
102 |
private val log_area = |
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
103 |
new TextArea { |
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
104 |
editable = false |
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
105 |
font = GUI.copy_font((new Label).font) |
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
106 |
} |
76023 | 107 |
private val scroll_log_area = new ScrollPane(log_area) |
108 |
||
76606 | 109 |
def log_progress(): Document_Editor.Log_Progress = |
110 |
new Document_Editor.Log_Progress(PIDE.session) { |
|
76491 | 111 |
override def show(text: String): Unit = |
112 |
if (text != log_area.text) { |
|
113 |
log_area.text = text |
|
114 |
val vertical = scroll_log_area.peer.getVerticalScrollBar |
|
115 |
vertical.setValue(vertical.getMaximum) |
|
116 |
} |
|
76023 | 117 |
} |
76021
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
118 |
|
75816 | 119 |
|
120 |
/* document build process */ |
|
121 |
||
76491 | 122 |
private def init_state(): Unit = |
76606 | 123 |
current_state.change { _ => Document_Dockable.State(progress = log_progress()) } |
76491 | 124 |
|
76718 | 125 |
private def cancel_process(): Unit = |
126 |
current_state.change { st => st.process.cancel(); st } |
|
127 |
||
128 |
private def await_process(): Unit = |
|
129 |
current_state.guarded_access(st => if (st.process.is_finished) None else Some((), st)) |
|
130 |
||
131 |
private def finish_process(output: List[XML.Tree]): Unit = |
|
132 |
current_state.change(_.finish(output)) |
|
133 |
||
134 |
private def run_process(body: Document_Editor.Log_Progress => Unit): Boolean = { |
|
135 |
val started = |
|
136 |
current_state.change_result { st => |
|
137 |
if (st.process.is_finished) { |
|
138 |
val progress = log_progress() |
|
139 |
val process = |
|
140 |
Future.thread[Unit](name = "Document_Dockable.process") { |
|
141 |
await_process() |
|
142 |
body(progress) |
|
143 |
} |
|
144 |
(true, st.run(progress, process)) |
|
145 |
} |
|
146 |
else (false, st) |
|
147 |
} |
|
148 |
show_state() |
|
149 |
started |
|
150 |
} |
|
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76711
diff
changeset
|
151 |
|
76681 | 152 |
private def load_document(session: String): Boolean = { |
76718 | 153 |
val options = PIDE.options.value |
76727 | 154 |
run_process { _ => |
76718 | 155 |
try { |
156 |
val session_background = |
|
157 |
Document_Build.session_background( |
|
158 |
options, session, dirs = JEdit_Sessions.session_dirs) |
|
159 |
PIDE.editor.document_setup(Some(session_background)) |
|
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76711
diff
changeset
|
160 |
|
76718 | 161 |
finish_process(Nil) |
162 |
GUI_Thread.later { |
|
76725
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
163 |
refresh_theories() |
76718 | 164 |
show_state() |
165 |
show_page(theories_page) |
|
166 |
} |
|
167 |
} |
|
168 |
catch { |
|
169 |
case exn: Throwable if !Exn.is_interrupt(exn) => |
|
170 |
finish_process(List(Protocol.error_message(Exn.print(exn)))) |
|
171 |
GUI_Thread.later { |
|
172 |
show_state() |
|
173 |
show_page(output_page) |
|
76681 | 174 |
} |
175 |
} |
|
176 |
} |
|
177 |
} |
|
178 |
||
76023 | 179 |
private def build_document(): Unit = { |
76718 | 180 |
run_process { progress => |
181 |
show_page(theories_page) |
|
182 |
Time.seconds(2.0).sleep() |
|
76567 | 183 |
|
76718 | 184 |
show_page(log_page) |
185 |
val res = |
|
186 |
Exn.capture { |
|
187 |
progress.echo("Start " + Date.now()) |
|
188 |
for (i <- 1 to 200) { |
|
189 |
progress.echo("message " + i) |
|
190 |
Time.seconds(0.1).sleep() |
|
191 |
} |
|
192 |
progress.echo("Stop " + Date.now()) |
|
193 |
} |
|
194 |
val msg = |
|
195 |
res match { |
|
196 |
case Exn.Res(_) => Protocol.writeln_message("OK") |
|
197 |
case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn)) |
|
198 |
} |
|
199 |
finish_process(List(msg)) |
|
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76711
diff
changeset
|
200 |
|
76718 | 201 |
show_state() |
76568 | 202 |
|
76718 | 203 |
show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page) |
204 |
GUI_Thread.later { progress.load() } |
|
76023 | 205 |
} |
206 |
} |
|
207 |
||
75816 | 208 |
|
209 |
/* controls */ |
|
210 |
||
76681 | 211 |
private val document_session = |
212 |
JEdit_Sessions.document_selector(PIDE.options, standalone = true) |
|
213 |
||
76602 | 214 |
private lazy val delay_load: Delay = |
76610 | 215 |
Delay.last(PIDE.session.load_delay, gui = true) { |
76681 | 216 |
for (session <- document_session.selection_value) { |
217 |
if (!load_document(session)) delay_load.invoke() |
|
218 |
} |
|
76602 | 219 |
} |
220 |
||
221 |
document_session.reactions += { case SelectionChanged(_) => delay_load.invoke() } |
|
222 |
||
76726 | 223 |
private val load_button = |
224 |
new GUI.Button("Load") { |
|
225 |
tooltip = "Load document theories" |
|
226 |
override def clicked(): Unit = PIDE.editor.document_select_all(set = true) |
|
227 |
} |
|
228 |
||
75853 | 229 |
private val build_button = |
230 |
new GUI.Button("<html><b>Build</b></html>") { |
|
75816 | 231 |
tooltip = "Build document" |
76023 | 232 |
override def clicked(): Unit = build_document() |
233 |
} |
|
234 |
||
235 |
private val cancel_button = |
|
236 |
new GUI.Button("Cancel") { |
|
237 |
tooltip = "Cancel build process" |
|
76718 | 238 |
override def clicked(): Unit = cancel_process() |
76023 | 239 |
} |
240 |
||
241 |
private val view_button = |
|
242 |
new GUI.Button("View") { |
|
243 |
tooltip = "View document" |
|
76606 | 244 |
override def clicked(): Unit = Document_Editor.view_document() |
75816 | 245 |
} |
246 |
||
247 |
private val controls = |
|
76726 | 248 |
Wrap_Panel(List(document_session, process_indicator.component, load_button, |
249 |
build_button, view_button, cancel_button)) |
|
75816 | 250 |
|
251 |
add(controls.peer, BorderLayout.NORTH) |
|
252 |
||
253 |
override def focusOnDefaultComponent(): Unit = build_button.requestFocus() |
|
254 |
||
255 |
||
76023 | 256 |
/* message pane with pages */ |
257 |
||
76726 | 258 |
private val reset_button = |
259 |
new GUI.Button("Reset") { |
|
260 |
tooltip = "Deselect document theories" |
|
76720 | 261 |
override def clicked(): Unit = PIDE.editor.document_select_all(set = false) |
262 |
} |
|
263 |
||
76726 | 264 |
private val purge_button = new GUI.Button("Purge") { |
265 |
tooltip = "Remove theories that are no longer required" |
|
266 |
override def clicked(): Unit = PIDE.editor.purge() |
|
267 |
} |
|
268 |
||
76720 | 269 |
private val theories_controls = |
76726 | 270 |
Wrap_Panel(List(reset_button, purge_button)) |
76720 | 271 |
|
76602 | 272 |
private val theories = new Theories_Status(view, document = true) |
76567 | 273 |
|
76725
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
274 |
private def refresh_theories(): Unit = { |
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
275 |
val domain = PIDE.editor.document_theories().toSet |
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
276 |
theories.update(domain = Some(domain), trim = true, force = true) |
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
277 |
theories.refresh() |
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
278 |
} |
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
279 |
|
76567 | 280 |
private val theories_page = |
281 |
new TabbedPane.Page("Theories", new BorderPanel { |
|
76720 | 282 |
layout(theories_controls) = BorderPanel.Position.North |
76567 | 283 |
layout(theories.gui) = BorderPanel.Position.Center |
284 |
}, "Selection and status of document theories") |
|
285 |
||
76023 | 286 |
private val output_controls = |
287 |
Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom)) |
|
288 |
||
289 |
private val output_page = |
|
290 |
new TabbedPane.Page("Output", new BorderPanel { |
|
291 |
layout(output_controls) = BorderPanel.Position.North |
|
292 |
layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center |
|
293 |
}, "Output from build process") |
|
294 |
||
295 |
private val log_page = |
|
296 |
new TabbedPane.Page("Log", new BorderPanel { |
|
76489
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
297 |
layout(scroll_log_area) = BorderPanel.Position.Center |
76023 | 298 |
}, "Raw log of build process") |
299 |
||
76567 | 300 |
message_pane.pages ++= List(theories_page, log_page, output_page) |
76023 | 301 |
|
302 |
set_content(message_pane) |
|
303 |
||
304 |
||
75816 | 305 |
/* main */ |
306 |
||
307 |
private val main = |
|
76567 | 308 |
Session.Consumer[Any](getClass.getName) { |
75816 | 309 |
case _: Session.Global_Options => |
76567 | 310 |
GUI_Thread.later { |
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76577
diff
changeset
|
311 |
document_session.load() |
76567 | 312 |
handle_resize() |
76725
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
313 |
refresh_theories() |
76567 | 314 |
} |
315 |
case changed: Session.Commands_Changed => |
|
316 |
GUI_Thread.later { |
|
76719 | 317 |
val domain = PIDE.editor.document_theories().filter(changed.nodes).toSet |
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76711
diff
changeset
|
318 |
if (domain.nonEmpty) theories.update(domain = Some(domain)) |
76567 | 319 |
} |
75816 | 320 |
} |
321 |
||
322 |
override def init(): Unit = { |
|
76701 | 323 |
PIDE.editor.document_init(dockable) |
76491 | 324 |
init_state() |
75816 | 325 |
PIDE.session.global_options += main |
76567 | 326 |
PIDE.session.commands_changed += main |
75816 | 327 |
handle_resize() |
76602 | 328 |
delay_load.invoke() |
75816 | 329 |
} |
330 |
||
331 |
override def exit(): Unit = { |
|
332 |
PIDE.session.global_options -= main |
|
76567 | 333 |
PIDE.session.commands_changed -= main |
75816 | 334 |
delay_resize.revoke() |
76701 | 335 |
PIDE.editor.document_exit(dockable) |
75816 | 336 |
} |
337 |
} |