# HG changeset patch # User wenzelm # Date 1673896095 -3600 # Node ID 7c23db6b857b2549888948c3daf9fce0ad5c3f78 # Parent a6d147b22b9b3c46934d00acc470ef0910a354f0 more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup; more Document_Build.running_script, but display it as "Running XYZ"; diff -r a6d147b22b9b -r 7c23db6b857b src/Pure/PIDE/document_editor.scala --- a/src/Pure/PIDE/document_editor.scala Mon Jan 16 13:48:03 2023 +0100 +++ b/src/Pure/PIDE/document_editor.scala Mon Jan 16 20:08:15 2023 +0100 @@ -20,27 +20,6 @@ } - /* progress */ - - class Log_Progress(session: Session) extends Progress { - def show(text: String): Unit = {} - - private val syslog = session.make_syslog() - - private def update(text: String = syslog.content()): Unit = show(text) - private val delay = Delay.first(session.update_delay, gui = true) { update() } - - override def echo(msg: String): Unit = { syslog += msg; delay.invoke() } - - def finish(text: String): Unit = GUI_Thread.require { - delay.revoke() - update(text) - } - - GUI_Thread.later { update() } - } - - /* configuration state */ sealed case class State( diff -r a6d147b22b9b -r 7c23db6b857b src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Mon Jan 16 13:48:03 2023 +0100 +++ b/src/Pure/System/progress.scala Mon Jan 16 20:08:15 2023 +0100 @@ -80,3 +80,89 @@ override def toString: String = path.toString } + + +/* structured program progress */ + +object Program_Progress { + class Program private[Program_Progress](title: String) { + private val output_buffer = new StringBuffer(256) // synchronized + + def echo(msg: String): Unit = synchronized { + if (output_buffer.length() > 0) output_buffer.append('\n') + output_buffer.append(msg) + } + + val start_time: Time = Time.now() + private var stop_time: Option[Time] = None + def stop_now(): Unit = synchronized { stop_time = Some(Time.now()) } + + def output(heading: String): (Command.Results, XML.Body) = synchronized { + val output_text = output_buffer.toString + val elapsed_time = stop_time.map(t => t - start_time) + + val message_prefix = heading + " " + val message_suffix = + elapsed_time match { + case None => " ..." + case Some(t) => " ... (" + t.message + " elapsed time)" + } + + val (results, message) = + if (output_text.isEmpty) { + (Command.Results.empty, XML.string(message_prefix + title + message_suffix)) + } + else { + val i = Document_ID.make() + val results = Command.Results.make(List(i -> Protocol.writeln_message(output_text))) + val message = + XML.string(message_prefix) ::: + List(XML.Elem(Markup(Markup.WRITELN, Markup.Serial(i)), XML.string(title))) ::: + XML.string(message_suffix) + (results, message) + } + + (results, List(XML.Elem(Markup(Markup.TRACING_MESSAGE, Nil), message))) + } + } +} + +abstract class Program_Progress extends Progress { + private var _finished_programs: List[Program_Progress.Program] = Nil + private var _running_program: Option[Program_Progress.Program] = None + + def output(heading: String = "Running"): (Command.Results, XML.Body) = synchronized { + val programs = (_running_program.toList ::: _finished_programs).reverse + val programs_output = programs.map(_.output(heading)) + val results = Command.Results.merge(programs_output.map(_._1)) + val body = Library.separate(Pretty.Separator, programs_output.map(_._2)).flatten + (results, body) + } + + private def start_program(title: String): Unit = synchronized { + _running_program = Some(new Program_Progress.Program(title)) + } + + def stop_program(): Unit = synchronized { + _running_program match { + case Some(program) => + program.stop_now() + _finished_programs ::= program + _running_program = None + case None => + } + } + + def detect_program(s: String): Option[String] + + override def echo(msg: String): Unit = synchronized { + detect_program(msg) match { + case Some(title) => + stop_program() + start_program(title) + case None => + if (_running_program.isEmpty) start_program("program") + _running_program.get.echo(msg) + } + } +} diff -r a6d147b22b9b -r 7c23db6b857b src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Mon Jan 16 13:48:03 2023 +0100 +++ b/src/Pure/Thy/document_build.scala Mon Jan 16 20:08:15 2023 +0100 @@ -132,9 +132,14 @@ List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty"). map(name => texinputs + Path.basic(name)) - def running_script(title: String): String = "echo 'Running " + quote(title) + " ...'; " - def is_running_script(msg: String): Boolean = - msg.startsWith("Running \"") && msg.endsWith("\" ...") + def running_script(title: String): String = + "echo " + Bash.string("Running program \"" + title + "\" ...") + ";" + + def detect_running_script(s: String): Option[String] = + for { + s1 <- Library.try_unprefix("Running program \"", s) + s2 <- Library.try_unsuffix("\" ...", s1) + } yield s2 sealed case class Document_Latex(name: Document.Node.Name, body: XML.Body) { def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body) diff -r a6d147b22b9b -r 7c23db6b857b src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Mon Jan 16 13:48:03 2023 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Mon Jan 16 20:08:15 2023 +0100 @@ -35,15 +35,25 @@ progress: Progress = new Progress, process: Future[Unit] = Future.value(()), status: Status.Value = Status.FINISHED, - output: List[XML.Tree] = Nil + output_results: Command.Results = Command.Results.empty, + output_main: XML.Body = Nil, + output_more: XML.Body = Nil ) { def run(progress: Progress, process: Future[Unit]): State = copy(progress = progress, process = process, status = Status.RUNNING) - def finish(output: List[XML.Tree]): State = - copy(process = Future.value(()), status = Status.FINISHED, output = output) + def running(results: Command.Results, body: XML.Body): State = + copy(status = Status.RUNNING, output_results = results, output_main = body) + + def finish(output: XML.Body): State = + copy(process = Future.value(()), status = Status.FINISHED, output_more = output) - def ok: Boolean = !output.exists(Protocol.is_error) + def output_body: XML.Body = + output_main ::: + (if (output_main.nonEmpty && output_more.nonEmpty) Pretty.Separator else Nil) ::: + output_more + + def ok: Boolean = !output_body.exists(Protocol.is_error) } } @@ -64,7 +74,7 @@ private def show_state(): Unit = GUI_Thread.later { val st = current_state.value - pretty_text_area.update(Document.Snapshot.init, Command.Results.empty, st.output) + pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_body) st.status match { case Document_Dockable.Status.WAITING => @@ -97,32 +107,34 @@ }) - /* progress log */ + /* progress */ - private val log_area = - new TextArea { - editable = false - font = GUI.copy_font((new Label).font) - } - private val scroll_log_area = new ScrollPane(log_area) + class Log_Progress extends Program_Progress { + progress => + + override def detect_program(s: String): Option[String] = + Document_Build.detect_running_script(s) - def log_progress(only_running: Boolean = false): Document_Editor.Log_Progress = - new Document_Editor.Log_Progress(PIDE.session) { - override def show(text: String): Unit = - if (text != log_area.text) { - log_area.text = text - val vertical = scroll_log_area.peer.getVerticalScrollBar - vertical.setValue(vertical.getMaximum) + private val delay: Delay = + Delay.first(PIDE.session.output_delay) { + if (!stopped) { + running_process(progress) + GUI_Thread.later { show_state() } } - override def echo(msg: String): Unit = - if (!only_running || Document_Build.is_running_script(msg)) super.echo(msg) - } + } + + override def echo(msg: String): Unit = { super.echo(msg); delay.invoke() } + override def stop_program(): Unit = { super.stop_program(); delay.invoke() } + } /* document build process */ private def init_state(): Unit = - current_state.change { _ => Document_Dockable.State(progress = log_progress()) } + current_state.change { st => + st.progress.stop() + Document_Dockable.State(progress = new Log_Progress) + } private def cancel_process(): Unit = current_state.change { st => st.process.cancel(); st } @@ -130,16 +142,20 @@ private def await_process(): Unit = current_state.guarded_access(st => if (st.process.is_finished) None else Some((), st)) - private def finish_process(output: List[XML.Tree]): Unit = + private def running_process(progress: Log_Progress): Unit = { + val (results, body) = progress.output() + current_state.change(_.running(results, body)) + } + + private def finish_process(output: XML.Body): Unit = current_state.change(_.finish(output)) - private def run_process(only_running: Boolean = false)( - body: Document_Editor.Log_Progress => Unit - ): Boolean = { + private def run_process(only_running: Boolean = false)(body: Log_Progress => Unit): Boolean = { val started = current_state.change_result { st => if (st.process.is_finished) { - val progress = log_progress(only_running = only_running) + st.progress.stop() + val progress = new Log_Progress val process = Future.thread[Unit](name = "Document_Dockable.process") { await_process() @@ -182,7 +198,7 @@ private def document_build( session_background: Sessions.Background, - progress: Document_Editor.Log_Progress + progress: Log_Progress ): Unit = { val store = JEdit_Sessions.sessions_store(PIDE.options.value) val document_selection = PIDE.editor.document_selection() @@ -197,16 +213,13 @@ document_session = Some(session_background.base), document_selection = document_selection, progress = progress) + val variant = session_background.info.documents.head Isabelle_System.make_directory(Document_Editor.document_output_dir()) val doc = context.build_document(variant, verbose = true) - // log File.write(Document_Editor.document_output().log, doc.log) - GUI_Thread.later { progress.finish(doc.log) } - - // pdf Bytes.write(Document_Editor.document_output().pdf, doc.pdf) Document_Editor.view_document() } @@ -217,7 +230,7 @@ PIDE.editor.document_session() match { case Some(session_background) if session_background.info.documents.nonEmpty => run_process(only_running = true) { progress => - show_page(log_page) + show_page(output_page) val result = Exn.capture { document_build(session_background, progress) } val msgs = result match { @@ -229,6 +242,8 @@ List(Protocol.error_message(YXML.parse_body(Exn.print(exn)))) } + progress.stop_program() + running_process(progress) finish_process(Pretty.separate(msgs)) show_state() @@ -325,12 +340,7 @@ layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center }, "Output from build process") - private val log_page = - new TabbedPane.Page("Log", new BorderPanel { - layout(scroll_log_area) = BorderPanel.Position.Center - }, "Raw log of build process") - - message_pane.pages ++= List(theories_page, log_page, output_page) + message_pane.pages ++= List(theories_page, output_page) set_content(message_pane)