author | wenzelm |
Tue, 31 Jan 2023 17:08:16 +0100 | |
changeset 77151 | 2f43be96c713 |
parent 77150 | 286fdf0fcc44 |
child 77152 | 4c9296390f20 |
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 State { |
76681 | 25 |
def init(): State = State() |
76023 | 26 |
} |
27 |
||
28 |
sealed case class State( |
|
77146 | 29 |
pending: Boolean = false, |
76023 | 30 |
process: Future[Unit] = Future.value(()), |
77146 | 31 |
progress: Progress = new Progress, |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
32 |
output_results: Command.Results = Command.Results.empty, |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
33 |
output_main: XML.Body = Nil, |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
34 |
output_more: XML.Body = Nil |
76681 | 35 |
) { |
77146 | 36 |
def running: Boolean = !process.is_finished |
76681 | 37 |
|
77147 | 38 |
def run(process: Future[Unit], progress: Progress, reset_pending: Boolean): State = |
39 |
copy(process = process, progress = progress, pending = if (reset_pending) false else pending) |
|
77146 | 40 |
|
41 |
def output(results: Command.Results, body: XML.Body): State = |
|
42 |
copy(output_results = results, output_main = body) |
|
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
43 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
44 |
def finish(output: XML.Body): State = |
77146 | 45 |
copy(process = Future.value(()), output_more = output) |
76718 | 46 |
|
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
47 |
def output_body: XML.Body = |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
48 |
output_main ::: |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
49 |
(if (output_main.nonEmpty && output_more.nonEmpty) Pretty.Separator else Nil) ::: |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
50 |
output_more |
76681 | 51 |
} |
76023 | 52 |
} |
53 |
||
75816 | 54 |
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
|
55 |
dockable => |
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
56 |
|
75816 | 57 |
GUI_Thread.require {} |
58 |
||
59 |
||
76023 | 60 |
/* component state -- owned by GUI thread */ |
61 |
||
76681 | 62 |
private val current_state = Synchronized(Document_Dockable.State.init()) |
76023 | 63 |
|
64 |
private val process_indicator = new Process_Indicator |
|
65 |
private val pretty_text_area = new Pretty_Text_Area(view) |
|
66 |
private val message_pane = new TabbedPane |
|
67 |
||
76034 | 68 |
private def show_state(): Unit = GUI_Thread.later { |
76023 | 69 |
val st = current_state.value |
70 |
||
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
71 |
pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_body) |
75816 | 72 |
|
77146 | 73 |
if (st.running) process_indicator.update("Running document build process ...", 15) |
74 |
else if (st.pending) process_indicator.update("Waiting for pending document content ...", 5) |
|
75 |
else process_indicator.update(null, 0) |
|
76034 | 76 |
} |
76023 | 77 |
|
76034 | 78 |
private def show_page(page: TabbedPane.Page): Unit = GUI_Thread.later { |
79 |
message_pane.selection.page = page |
|
76023 | 80 |
} |
81 |
||
82 |
||
83 |
/* text area with zoom/resize */ |
|
75816 | 84 |
|
85 |
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation |
|
86 |
||
76021
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
87 |
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
|
88 |
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
|
89 |
|
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
90 |
private val delay_resize: Delay = |
76610 | 91 |
Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } |
76021
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
92 |
|
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
93 |
addComponentListener(new ComponentAdapter { |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
94 |
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
95 |
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
96 |
}) |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
97 |
|
76023 | 98 |
|
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
99 |
/* progress */ |
76023 | 100 |
|
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
101 |
class Log_Progress extends Program_Progress { |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
102 |
progress => |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
103 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
104 |
override def detect_program(s: String): Option[String] = |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
105 |
Document_Build.detect_running_script(s) |
76023 | 106 |
|
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
107 |
private val delay: Delay = |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
108 |
Delay.first(PIDE.session.output_delay) { |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
109 |
if (!stopped) { |
77146 | 110 |
output_process(progress) |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
111 |
GUI_Thread.later { show_state() } |
76491 | 112 |
} |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
113 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
114 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
115 |
override def echo(msg: String): Unit = { super.echo(msg); delay.invoke() } |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
116 |
override def stop_program(): Unit = { super.stop_program(); delay.invoke() } |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
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 = |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
123 |
current_state.change { st => |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
124 |
st.progress.stop() |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
125 |
Document_Dockable.State(progress = new Log_Progress) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
126 |
} |
76491 | 127 |
|
76718 | 128 |
private def cancel_process(): Unit = |
129 |
current_state.change { st => st.process.cancel(); st } |
|
130 |
||
131 |
private def await_process(): Unit = |
|
132 |
current_state.guarded_access(st => if (st.process.is_finished) None else Some((), st)) |
|
133 |
||
77146 | 134 |
private def output_process(progress: Log_Progress): Unit = { |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
135 |
val (results, body) = progress.output() |
77146 | 136 |
current_state.change(_.output(results, body)) |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
137 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
138 |
|
77147 | 139 |
private def pending_process(): Unit = |
140 |
current_state.change { st => |
|
141 |
if (st.pending) st |
|
77149
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
142 |
else { |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
143 |
delay_auto_build.revoke() |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
144 |
delay_build.invoke() |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
145 |
st.copy(pending = true) |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
146 |
} |
77147 | 147 |
} |
148 |
||
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
149 |
private def finish_process(output: XML.Body): Unit = |
77147 | 150 |
current_state.change { st => |
77149
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
151 |
if (st.pending) { |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
152 |
delay_auto_build.revoke() |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
153 |
delay_build.invoke() |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
154 |
} |
77147 | 155 |
st.finish(output) |
156 |
} |
|
76718 | 157 |
|
77147 | 158 |
private def run_process(reset_pending: Boolean = false)(body: Log_Progress => Unit): Boolean = { |
76718 | 159 |
val started = |
160 |
current_state.change_result { st => |
|
161 |
if (st.process.is_finished) { |
|
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
162 |
st.progress.stop() |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
163 |
val progress = new Log_Progress |
76718 | 164 |
val process = |
165 |
Future.thread[Unit](name = "Document_Dockable.process") { |
|
166 |
await_process() |
|
167 |
body(progress) |
|
168 |
} |
|
77147 | 169 |
(true, st.run(process, progress, reset_pending)) |
76718 | 170 |
} |
171 |
else (false, st) |
|
172 |
} |
|
173 |
show_state() |
|
174 |
started |
|
175 |
} |
|
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76711
diff
changeset
|
176 |
|
76681 | 177 |
private def load_document(session: String): Boolean = { |
76718 | 178 |
val options = PIDE.options.value |
77147 | 179 |
run_process() { _ => |
76718 | 180 |
try { |
181 |
val session_background = |
|
182 |
Document_Build.session_background( |
|
183 |
options, session, dirs = JEdit_Sessions.session_dirs) |
|
184 |
PIDE.editor.document_setup(Some(session_background)) |
|
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76711
diff
changeset
|
185 |
|
76718 | 186 |
finish_process(Nil) |
187 |
GUI_Thread.later { |
|
76725
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
188 |
refresh_theories() |
76718 | 189 |
show_state() |
76996 | 190 |
show_page(input_page) |
76718 | 191 |
} |
192 |
} |
|
193 |
catch { |
|
194 |
case exn: Throwable if !Exn.is_interrupt(exn) => |
|
195 |
finish_process(List(Protocol.error_message(Exn.print(exn)))) |
|
196 |
GUI_Thread.later { |
|
197 |
show_state() |
|
198 |
show_page(output_page) |
|
76681 | 199 |
} |
200 |
} |
|
201 |
} |
|
202 |
} |
|
203 |
||
76732 | 204 |
private def document_build( |
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
205 |
document_session: Document_Editor.Session, |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
206 |
progress: Log_Progress |
76732 | 207 |
): Unit = { |
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
208 |
val session_background = document_session.get_background |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
209 |
val snapshot = document_session.get_snapshot |
77022 | 210 |
val session_context = JEdit_Sessions.open_session_context(document_snapshot = Some(snapshot)) |
76732 | 211 |
try { |
212 |
val context = |
|
213 |
Document_Build.context(session_context, |
|
214 |
document_session = Some(session_background.base), |
|
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
215 |
document_selection = document_session.selection, |
76732 | 216 |
progress = progress) |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76769
diff
changeset
|
217 |
|
76732 | 218 |
Isabelle_System.make_directory(Document_Editor.document_output_dir()) |
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
219 |
val doc = context.build_document(document_session.get_variant, verbose = true) |
76732 | 220 |
|
221 |
File.write(Document_Editor.document_output().log, doc.log) |
|
222 |
Bytes.write(Document_Editor.document_output().pdf, doc.pdf) |
|
223 |
Document_Editor.view_document() |
|
224 |
} |
|
225 |
finally { session_context.close() } |
|
226 |
} |
|
227 |
||
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
228 |
private def document_build_attempt(): Boolean = { |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
229 |
val document_session = PIDE.editor.document_session() |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
230 |
if (document_session.is_vacuous) true |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
231 |
else if (document_session.is_pending) false |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
232 |
else { |
77147 | 233 |
run_process(reset_pending = true) { progress => |
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
234 |
show_page(output_page) |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
235 |
val result = Exn.capture { document_build(document_session, progress) } |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
236 |
val msgs = |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
237 |
result match { |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
238 |
case Exn.Res(_) => |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
239 |
List(Protocol.writeln_message("OK")) |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
240 |
case Exn.Exn(exn: Document_Build.Build_Error) => |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
241 |
exn.log_errors.map(s => Protocol.error_message(YXML.parse_body(s))) |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
242 |
case Exn.Exn(exn) => |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
243 |
List(Protocol.error_message(YXML.parse_body(Exn.print(exn)))) |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
244 |
} |
76732 | 245 |
|
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
246 |
progress.stop_program() |
77146 | 247 |
output_process(progress) |
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
248 |
finish_process(Pretty.separate(msgs)) |
76732 | 249 |
|
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
250 |
show_state() |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
251 |
show_page(if (Exn.is_interrupt_exn(result)) input_page else output_page) |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
252 |
} |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
253 |
true |
76023 | 254 |
} |
255 |
} |
|
256 |
||
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
257 |
private lazy val delay_build: Delay = |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
258 |
Delay.first(PIDE.session.output_delay, gui = true) { |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
259 |
if (!document_build_attempt()) delay_build.invoke() |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
260 |
} |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
77142
diff
changeset
|
261 |
|
77149
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
262 |
private lazy val delay_auto_build: Delay = |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
263 |
Delay.last(PIDE.session.document_delay, gui = true) { |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
264 |
pending_process() |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
265 |
} |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
266 |
|
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
267 |
private def document_pending() = current_state.value.pending |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
268 |
|
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
269 |
private val document_auto = new JEdit_Options.Bool_Access("editor_document_auto") |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
270 |
|
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
271 |
|
75816 | 272 |
|
273 |
/* controls */ |
|
274 |
||
76681 | 275 |
private val document_session = |
276 |
JEdit_Sessions.document_selector(PIDE.options, standalone = true) |
|
277 |
||
76602 | 278 |
private lazy val delay_load: Delay = |
76610 | 279 |
Delay.last(PIDE.session.load_delay, gui = true) { |
76681 | 280 |
for (session <- document_session.selection_value) { |
281 |
if (!load_document(session)) delay_load.invoke() |
|
282 |
} |
|
76602 | 283 |
} |
284 |
||
285 |
document_session.reactions += { case SelectionChanged(_) => delay_load.invoke() } |
|
286 |
||
76726 | 287 |
private val load_button = |
288 |
new GUI.Button("Load") { |
|
289 |
tooltip = "Load document theories" |
|
290 |
override def clicked(): Unit = PIDE.editor.document_select_all(set = true) |
|
291 |
} |
|
292 |
||
77149
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
293 |
private val auto_build_button = |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
294 |
new JEdit_Options.Bool_GUI(document_auto, "Auto") { |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
295 |
tooltip = Word.capitalize(document_auto.description) |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
296 |
override def clicked(state: Boolean): Unit = { |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
297 |
super.clicked(state) |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
298 |
if (state) delay_auto_build.invoke() |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
299 |
} |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
300 |
} |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
301 |
|
75853 | 302 |
private val build_button = |
303 |
new GUI.Button("<html><b>Build</b></html>") { |
|
75816 | 304 |
tooltip = "Build document" |
77147 | 305 |
override def clicked(): Unit = pending_process() |
76023 | 306 |
} |
307 |
||
308 |
private val cancel_button = |
|
309 |
new GUI.Button("Cancel") { |
|
310 |
tooltip = "Cancel build process" |
|
76718 | 311 |
override def clicked(): Unit = cancel_process() |
76023 | 312 |
} |
313 |
||
314 |
private val view_button = |
|
315 |
new GUI.Button("View") { |
|
316 |
tooltip = "View document" |
|
76606 | 317 |
override def clicked(): Unit = Document_Editor.view_document() |
75816 | 318 |
} |
319 |
||
320 |
private val controls = |
|
76726 | 321 |
Wrap_Panel(List(document_session, process_indicator.component, load_button, |
77149
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
322 |
auto_build_button, build_button, view_button, cancel_button)) |
75816 | 323 |
|
324 |
add(controls.peer, BorderLayout.NORTH) |
|
325 |
||
326 |
override def focusOnDefaultComponent(): Unit = build_button.requestFocus() |
|
327 |
||
328 |
||
76023 | 329 |
/* message pane with pages */ |
330 |
||
76726 | 331 |
private val reset_button = |
332 |
new GUI.Button("Reset") { |
|
333 |
tooltip = "Deselect document theories" |
|
76720 | 334 |
override def clicked(): Unit = PIDE.editor.document_select_all(set = false) |
335 |
} |
|
336 |
||
76726 | 337 |
private val purge_button = new GUI.Button("Purge") { |
338 |
tooltip = "Remove theories that are no longer required" |
|
339 |
override def clicked(): Unit = PIDE.editor.purge() |
|
340 |
} |
|
341 |
||
76720 | 342 |
private val theories_controls = |
76726 | 343 |
Wrap_Panel(List(reset_button, purge_button)) |
76720 | 344 |
|
76602 | 345 |
private val theories = new Theories_Status(view, document = true) |
77008 | 346 |
private val theories_pane = new ScrollPane(theories.gui) |
76567 | 347 |
|
76725
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
348 |
private def refresh_theories(): Unit = { |
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
349 |
val domain = PIDE.editor.document_theories().toSet |
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
350 |
theories.update(domain = Some(domain), trim = true, force = true) |
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
351 |
theories.refresh() |
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
352 |
} |
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
353 |
|
76996 | 354 |
private val input_page = |
355 |
new TabbedPane.Page("Input", new BorderPanel { |
|
76720 | 356 |
layout(theories_controls) = BorderPanel.Position.North |
77008 | 357 |
layout(theories_pane) = BorderPanel.Position.Center |
76567 | 358 |
}, "Selection and status of document theories") |
359 |
||
76023 | 360 |
private val output_controls = |
361 |
Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom)) |
|
362 |
||
363 |
private val output_page = |
|
364 |
new TabbedPane.Page("Output", new BorderPanel { |
|
365 |
layout(output_controls) = BorderPanel.Position.North |
|
366 |
layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center |
|
76996 | 367 |
}, "Results from document build process") |
76023 | 368 |
|
76996 | 369 |
message_pane.pages ++= List(input_page, output_page) |
76023 | 370 |
|
371 |
set_content(message_pane) |
|
372 |
||
373 |
||
75816 | 374 |
/* main */ |
375 |
||
376 |
private val main = |
|
76567 | 377 |
Session.Consumer[Any](getClass.getName) { |
75816 | 378 |
case _: Session.Global_Options => |
76567 | 379 |
GUI_Thread.later { |
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76577
diff
changeset
|
380 |
document_session.load() |
76567 | 381 |
handle_resize() |
76725
c8d5cc19270a
more thorough GUI updates, notably for multiple Document dockables;
wenzelm
parents:
76720
diff
changeset
|
382 |
refresh_theories() |
76567 | 383 |
} |
384 |
case changed: Session.Commands_Changed => |
|
385 |
GUI_Thread.later { |
|
76719 | 386 |
val domain = PIDE.editor.document_theories().filter(changed.nodes).toSet |
77150 | 387 |
if (domain.nonEmpty) { |
388 |
theories.update(domain = Some(domain)) |
|
77149
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
389 |
|
77150 | 390 |
val pending = document_pending() |
391 |
val auto = document_auto() |
|
392 |
if ((pending || auto) && PIDE.editor.document_session().is_ready) { |
|
77149
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
393 |
if (pending) { |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
394 |
delay_auto_build.revoke() |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
395 |
delay_build.invoke() |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
396 |
} |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
397 |
else if (auto) { |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
398 |
delay_auto_build.invoke() |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
399 |
} |
3991a35cd740
automatically build document when selected theories are finished;
wenzelm
parents:
77147
diff
changeset
|
400 |
} |
77147 | 401 |
} |
76567 | 402 |
} |
75816 | 403 |
} |
404 |
||
405 |
override def init(): Unit = { |
|
76701 | 406 |
PIDE.editor.document_init(dockable) |
76491 | 407 |
init_state() |
75816 | 408 |
PIDE.session.global_options += main |
76567 | 409 |
PIDE.session.commands_changed += main |
75816 | 410 |
handle_resize() |
76602 | 411 |
delay_load.invoke() |
75816 | 412 |
} |
413 |
||
414 |
override def exit(): Unit = { |
|
415 |
PIDE.session.global_options -= main |
|
76567 | 416 |
PIDE.session.commands_changed -= main |
75816 | 417 |
delay_resize.revoke() |
76701 | 418 |
PIDE.editor.document_exit(dockable) |
75816 | 419 |
} |
420 |
} |