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