author | wenzelm |
Thu, 10 Nov 2022 12:21:44 +0100 | |
changeset 76504 | 15b058bb2416 |
parent 76494 | 9686049ce988 |
child 76562 | 9c5780693350 |
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} |
16 |
||
75816 | 17 |
import org.gjt.sp.jedit.{jEdit, View} |
18 |
||
19 |
||
76023 | 20 |
object Document_Dockable { |
76491 | 21 |
/* document output */ |
22 |
||
23 |
def document_name: String = "document" |
|
24 |
def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output") |
|
25 |
def document_output(): Path = document_output_dir() + Path.basic(document_name) |
|
26 |
||
27 |
def view_document(): Unit = { |
|
28 |
val path = Document_Dockable.document_output().pdf |
|
29 |
if (path.is_file) Isabelle_System.pdf_viewer(path) |
|
76490 | 30 |
} |
76023 | 31 |
|
76491 | 32 |
class Log_Progress extends Progress { |
33 |
def show(text: String): Unit = {} |
|
34 |
||
35 |
private val syslog = PIDE.session.make_syslog() |
|
36 |
||
37 |
private def update(text: String = syslog.content()): Unit = GUI_Thread.require { show(text) } |
|
38 |
private val delay = |
|
39 |
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { update() } |
|
40 |
||
41 |
override def echo(msg: String): Unit = { syslog += msg; delay.invoke() } |
|
42 |
override def theory(theory: Progress.Theory): Unit = echo(theory.message) |
|
43 |
||
44 |
def load(): Unit = { |
|
45 |
val path = document_output().log |
|
46 |
val text = if (path.is_file) File.read(path) else "" |
|
47 |
GUI_Thread.later { delay.revoke(); update(text) } |
|
48 |
} |
|
49 |
||
50 |
update() |
|
51 |
} |
|
52 |
||
53 |
||
54 |
/* state */ |
|
55 |
||
76023 | 56 |
object Status extends Enumeration { |
57 |
val WAITING = Value("waiting") |
|
58 |
val RUNNING = Value("running") |
|
59 |
val FINISHED = Value("finished") |
|
60 |
} |
|
61 |
||
76026 | 62 |
sealed case class Result(output: List[XML.Tree] = Nil) { |
63 |
def failed: Boolean = output.exists(Protocol.is_error) |
|
64 |
} |
|
76023 | 65 |
|
66 |
object State { |
|
76491 | 67 |
def empty(): State = State() |
76026 | 68 |
def finish(result: Result): State = State(output = result.output) |
76023 | 69 |
} |
70 |
||
71 |
sealed case class State( |
|
76491 | 72 |
progress: Log_Progress = new Log_Progress, |
76023 | 73 |
process: Future[Unit] = Future.value(()), |
74 |
output: List[XML.Tree] = Nil, |
|
76491 | 75 |
status: Status.Value = Status.FINISHED) |
76023 | 76 |
} |
77 |
||
75816 | 78 |
class Document_Dockable(view: View, position: String) extends Dockable(view, position) { |
79 |
GUI_Thread.require {} |
|
80 |
||
81 |
||
76023 | 82 |
/* component state -- owned by GUI thread */ |
83 |
||
76491 | 84 |
private val current_state = Synchronized(Document_Dockable.State.empty()) |
76023 | 85 |
|
86 |
private val process_indicator = new Process_Indicator |
|
87 |
private val pretty_text_area = new Pretty_Text_Area(view) |
|
88 |
private val message_pane = new TabbedPane |
|
89 |
||
76034 | 90 |
private def show_state(): Unit = GUI_Thread.later { |
76023 | 91 |
val st = current_state.value |
92 |
||
93 |
pretty_text_area.update(Document.Snapshot.init, Command.Results.empty, st.output) |
|
75816 | 94 |
|
76023 | 95 |
st.status match { |
96 |
case Document_Dockable.Status.WAITING => |
|
97 |
process_indicator.update("Waiting for PIDE document content ...", 5) |
|
98 |
case Document_Dockable.Status.RUNNING => |
|
99 |
process_indicator.update("Running document build process ...", 15) |
|
100 |
case Document_Dockable.Status.FINISHED => |
|
101 |
process_indicator.update(null, 0) |
|
102 |
} |
|
76034 | 103 |
} |
76023 | 104 |
|
76034 | 105 |
private def show_page(page: TabbedPane.Page): Unit = GUI_Thread.later { |
106 |
message_pane.selection.page = page |
|
76023 | 107 |
} |
108 |
||
109 |
||
110 |
/* text area with zoom/resize */ |
|
75816 | 111 |
|
112 |
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation |
|
113 |
||
76021
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
114 |
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
|
115 |
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
|
116 |
|
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
117 |
private val delay_resize: Delay = |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
118 |
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
119 |
|
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
120 |
addComponentListener(new ComponentAdapter { |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
121 |
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
122 |
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
123 |
}) |
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
124 |
|
76023 | 125 |
|
126 |
/* progress log */ |
|
127 |
||
76489
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
128 |
private val log_area = |
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
129 |
new TextArea { |
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
130 |
editable = false |
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
131 |
font = GUI.copy_font((new Label).font) |
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
132 |
} |
76023 | 133 |
private val scroll_log_area = new ScrollPane(log_area) |
134 |
||
76491 | 135 |
def init_progress(): Document_Dockable.Log_Progress = |
136 |
new Document_Dockable.Log_Progress { |
|
137 |
override def show(text: String): Unit = |
|
138 |
if (text != log_area.text) { |
|
139 |
log_area.text = text |
|
140 |
val vertical = scroll_log_area.peer.getVerticalScrollBar |
|
141 |
vertical.setValue(vertical.getMaximum) |
|
142 |
} |
|
76023 | 143 |
} |
76021
752425c69577
clarified component structure, concerning initialization order;
wenzelm
parents:
75853
diff
changeset
|
144 |
|
75816 | 145 |
|
146 |
/* document build process */ |
|
147 |
||
76023 | 148 |
private def cancel(): Unit = |
149 |
current_state.change { st => st.process.cancel(); st } |
|
150 |
||
76491 | 151 |
private def init_state(): Unit = |
152 |
current_state.change { _ => Document_Dockable.State(progress = init_progress()) } |
|
153 |
||
76023 | 154 |
private def build_document(): Unit = { |
155 |
current_state.change { st => |
|
156 |
if (st.process.is_finished) { |
|
76491 | 157 |
val progress = init_progress() |
76023 | 158 |
val process = |
159 |
Future.thread[Unit](name = "document_build") { |
|
76034 | 160 |
show_page(log_page) |
76023 | 161 |
val res = |
162 |
Exn.capture { |
|
163 |
progress.echo("Start " + Date.now()) |
|
76489
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
164 |
for (i <- 1 to 200) { |
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
165 |
progress.echo("message " + i) |
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
166 |
Time.seconds(0.1).sleep() |
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
167 |
} |
76023 | 168 |
progress.echo("Stop " + Date.now()) |
169 |
} |
|
76026 | 170 |
val msg = |
76023 | 171 |
res match { |
76026 | 172 |
case Exn.Res(_) => Protocol.make_message(XML.string("OK")) |
173 |
case Exn.Exn(exn) => Protocol.error_message(XML.string(Exn.message(exn))) |
|
76023 | 174 |
} |
76026 | 175 |
val result = Document_Dockable.Result(output = List(msg)) |
76035 | 176 |
current_state.change(_ => Document_Dockable.State.finish(result)) |
177 |
show_state() |
|
178 |
show_page(output_page) |
|
76023 | 179 |
} |
180 |
st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING) |
|
181 |
} |
|
182 |
else st |
|
183 |
} |
|
184 |
show_state() |
|
185 |
} |
|
186 |
||
75816 | 187 |
|
188 |
/* controls */ |
|
189 |
||
76492
e228be7cd375
clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents:
76491
diff
changeset
|
190 |
private val document_session: GUI.Selector[String] = { |
e228be7cd375
clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents:
76491
diff
changeset
|
191 |
val sessions = JEdit_Sessions.sessions_structure() |
e228be7cd375
clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents:
76491
diff
changeset
|
192 |
val all_sessions = sessions.build_topological_order.sorted |
e228be7cd375
clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents:
76491
diff
changeset
|
193 |
val doc_sessions = all_sessions.filter(name => sessions(name).doc_group) |
76504
15b058bb2416
clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;
wenzelm
parents:
76494
diff
changeset
|
194 |
new GUI.Selector[String]( |
15b058bb2416
clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;
wenzelm
parents:
76494
diff
changeset
|
195 |
doc_sessions.map(GUI.Selector.item), |
15b058bb2416
clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;
wenzelm
parents:
76494
diff
changeset
|
196 |
all_sessions.map(GUI.Selector.item) |
76492
e228be7cd375
clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents:
76491
diff
changeset
|
197 |
) { |
75830 | 198 |
val title = "Session" |
199 |
} |
|
76492
e228be7cd375
clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents:
76491
diff
changeset
|
200 |
} |
75830 | 201 |
|
75853 | 202 |
private val build_button = |
203 |
new GUI.Button("<html><b>Build</b></html>") { |
|
75816 | 204 |
tooltip = "Build document" |
76023 | 205 |
override def clicked(): Unit = build_document() |
206 |
} |
|
207 |
||
208 |
private val cancel_button = |
|
209 |
new GUI.Button("Cancel") { |
|
210 |
tooltip = "Cancel build process" |
|
211 |
override def clicked(): Unit = cancel() |
|
212 |
} |
|
213 |
||
214 |
private val view_button = |
|
215 |
new GUI.Button("View") { |
|
216 |
tooltip = "View document" |
|
76491 | 217 |
override def clicked(): Unit = Document_Dockable.view_document() |
75816 | 218 |
} |
219 |
||
220 |
private val controls = |
|
75830 | 221 |
Wrap_Panel(List(document_session, process_indicator.component, build_button, |
76023 | 222 |
view_button, cancel_button)) |
75816 | 223 |
|
224 |
add(controls.peer, BorderLayout.NORTH) |
|
225 |
||
226 |
override def focusOnDefaultComponent(): Unit = build_button.requestFocus() |
|
227 |
||
228 |
||
76023 | 229 |
/* message pane with pages */ |
230 |
||
231 |
private val output_controls = |
|
232 |
Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom)) |
|
233 |
||
234 |
private val output_page = |
|
235 |
new TabbedPane.Page("Output", new BorderPanel { |
|
236 |
layout(output_controls) = BorderPanel.Position.North |
|
237 |
layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center |
|
238 |
}, "Output from build process") |
|
239 |
||
76491 | 240 |
private val load_button = |
241 |
new GUI.Button("Load") { |
|
242 |
tooltip = "Load final log file" |
|
243 |
override def clicked(): Unit = current_state.value.progress.load() |
|
244 |
} |
|
245 |
||
246 |
private val log_controls = |
|
247 |
Wrap_Panel(List(load_button)) |
|
248 |
||
76023 | 249 |
private val log_page = |
250 |
new TabbedPane.Page("Log", new BorderPanel { |
|
76491 | 251 |
layout(log_controls) = BorderPanel.Position.North |
76489
8c9830109ab2
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents:
76036
diff
changeset
|
252 |
layout(scroll_log_area) = BorderPanel.Position.Center |
76023 | 253 |
}, "Raw log of build process") |
254 |
||
76036 | 255 |
message_pane.pages ++= List(log_page, output_page) |
76023 | 256 |
|
257 |
set_content(message_pane) |
|
258 |
||
259 |
||
75816 | 260 |
/* main */ |
261 |
||
262 |
private val main = |
|
263 |
Session.Consumer[Session.Global_Options](getClass.getName) { |
|
264 |
case _: Session.Global_Options => |
|
265 |
GUI_Thread.later { handle_resize() } |
|
266 |
} |
|
267 |
||
268 |
override def init(): Unit = { |
|
76491 | 269 |
init_state() |
75816 | 270 |
PIDE.session.global_options += main |
271 |
handle_resize() |
|
272 |
} |
|
273 |
||
274 |
override def exit(): Unit = { |
|
275 |
PIDE.session.global_options -= main |
|
276 |
delay_resize.revoke() |
|
277 |
} |
|
278 |
} |