# HG changeset patch # User wenzelm # Date 1661956758 -7200 # Node ID c7fed2fd52f5aeff599cfa83101d0a339f932bbb # Parent 6ce62e4e7dc0b3ca46f4fcb88fede10c924cf96d more GUI functionality; diff -r 6ce62e4e7dc0 -r c7fed2fd52f5 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Wed Aug 31 15:05:28 2022 +0200 +++ b/src/Tools/jEdit/src/document_dockable.scala Wed Aug 31 16:39:18 2022 +0200 @@ -12,16 +12,68 @@ import java.awt.BorderLayout import java.awt.event.{ComponentEvent, ComponentAdapter} +import scala.swing.{ScrollPane, TextArea, Label, TabbedPane, BorderPanel, Component} + import org.gjt.sp.jedit.{jEdit, View} +object Document_Dockable { + def document_output(): Path = + Path.explode("$ISABELLE_HOME_USER/document/root.pdf") + + object Status extends Enumeration { + val WAITING = Value("waiting") + val RUNNING = Value("running") + val FINISHED = Value("finished") + } + + sealed case class Result(output: List[XML.Tree] = Nil, ok: Boolean = true) + + object State { + val empty: State = State() + def finish(result: Result): State = State(ok = result.ok, output = result.output) + } + + sealed case class State( + progress: Progress = new Progress, + process: Future[Unit] = Future.value(()), + ok: Boolean = true, + output: List[XML.Tree] = Nil, + status: Status.Value = Status.FINISHED + ) +} + class Document_Dockable(view: View, position: String) extends Dockable(view, position) { GUI_Thread.require {} - /* text area with zoom/resize */ + /* component state -- owned by GUI thread */ + + private val current_state = Synchronized(Document_Dockable.State.empty) + + private val process_indicator = new Process_Indicator + private val pretty_text_area = new Pretty_Text_Area(view) + private val message_pane = new TabbedPane + + def show_state(): Unit = GUI_Thread.later { + val st = current_state.value + + pretty_text_area.update(Document.Snapshot.init, Command.Results.empty, st.output) - val pretty_text_area = new Pretty_Text_Area(view) + st.status match { + case Document_Dockable.Status.WAITING => + process_indicator.update("Waiting for PIDE document content ...", 5) + case Document_Dockable.Status.RUNNING => + process_indicator.update("Running document build process ...", 15) + case Document_Dockable.Status.FINISHED => + process_indicator.update(null, 0) + } + + if (!st.ok && output_page != null) message_pane.selection.page = output_page + } + + + /* text area with zoom/resize */ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation @@ -36,12 +88,74 @@ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() }) - set_content(pretty_text_area) + + /* progress log */ + + private val log_area = new TextArea { + editable = false + columns = 60 + rows = 24 + } + log_area.font = GUI.copy_font((new Label).font) + + private val scroll_log_area = new ScrollPane(log_area) + + private def init_progress() = { + GUI_Thread.later { log_area.text = "" } + new Progress { + override def echo(txt: String): Unit = + GUI_Thread.later { + log_area.append(txt + "\n") + val vertical = scroll_log_area.peer.getVerticalScrollBar + vertical.setValue(vertical.getMaximum) + } + + override def theory(theory: Progress.Theory): Unit = echo(theory.message) + } + } /* document build process */ - private val process_indicator = new Process_Indicator + private def cancel(): Unit = + current_state.change { st => st.process.cancel(); st } + + private def finish(result: Document_Dockable.Result): Unit = { + current_state.change { _ => Document_Dockable.State.finish(result) } + show_state() + } + + private def build_document(): Unit = { + current_state.change { st => + if (st.process.is_finished) { + val progress = init_progress() + val process = + Future.thread[Unit](name = "document_build") { + val res = + Exn.capture { + progress.echo("Start " + Date.now()) + Time.seconds(2.0).sleep() + progress.echo("Stop " + Date.now()) + } + val (ok, msg) = + res match { + case Exn.Res(_) => (true, Protocol.make_message(XML.string("OK"))) + case Exn.Exn(exn) => (false, Protocol.error_message(XML.string(Exn.message(exn)))) + } + val result = Document_Dockable.Result(ok = ok, output = List(msg)) + finish(result) + } + st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING) + } + else st + } + show_state() + } + + private def view_document(): Unit = { + val path = Document_Dockable.document_output() + if (path.is_file) Isabelle_System.pdf_viewer(path) + } /* controls */ @@ -54,22 +168,51 @@ private val build_button = new GUI.Button("Build") { tooltip = "Build document" - override def clicked(): Unit = { - pretty_text_area.update( - Document.Snapshot.init, Command.Results.empty, - List(XML.Text(Date.now().toString))) // FIXME - } + override def clicked(): Unit = build_document() + } + + private val cancel_button = + new GUI.Button("Cancel") { + tooltip = "Cancel build process" + override def clicked(): Unit = cancel() + } + + private val view_button = + new GUI.Button("View") { + tooltip = "View document" + override def clicked(): Unit = view_document() } private val controls = Wrap_Panel(List(document_session, process_indicator.component, build_button, - pretty_text_area.search_label, pretty_text_area.search_field, zoom)) + view_button, cancel_button)) add(controls.peer, BorderLayout.NORTH) override def focusOnDefaultComponent(): Unit = build_button.requestFocus() + /* message pane with pages */ + + private val output_controls = + Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom)) + + private val output_page = + new TabbedPane.Page("Output", new BorderPanel { + layout(output_controls) = BorderPanel.Position.North + layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center + }, "Output from build process") + + private val log_page = + new TabbedPane.Page("Log", new BorderPanel { + layout(log_area) = BorderPanel.Position.Center + }, "Raw log of build process") + + message_pane.pages ++= List(output_page, log_page) + + set_content(message_pane) + + /* main */ private val main =