# HG changeset patch # User wenzelm # Date 1671633273 -3600 # Node ID 0ba6f360d38a15fa44efff90a822d3cffae95235 # Parent 872fc664cd9975808f715965e4a036e4bb45abc6 actually build document; clarified signature; diff -r 872fc664cd99 -r 0ba6f360d38a src/Pure/PIDE/document_editor.scala --- a/src/Pure/PIDE/document_editor.scala Wed Dec 21 14:14:02 2022 +0100 +++ b/src/Pure/PIDE/document_editor.scala Wed Dec 21 15:34:33 2022 +0100 @@ -32,10 +32,9 @@ override def echo(msg: String): Unit = { syslog += msg; delay.invoke() } - def load(): Unit = GUI_Thread.require { - val path = document_output().log - val text = if (path.is_file) File.read(path) else "" - GUI_Thread.later { delay.revoke(); update(text) } + def finish(text: String): Unit = GUI_Thread.require { + delay.revoke() + update(text) } GUI_Thread.later { update() } diff -r 872fc664cd99 -r 0ba6f360d38a src/Pure/PIDE/editor.scala --- a/src/Pure/PIDE/editor.scala Wed Dec 21 14:14:02 2022 +0100 +++ b/src/Pure/PIDE/editor.scala Wed Dec 21 15:34:33 2022 +0100 @@ -40,6 +40,7 @@ def document_node_required(name: Document.Node.Name): Boolean = document_state().is_required(name) def document_theories(): List[Document.Node.Name] = document_state().active_document_theories + def document_selection(): Set[Document.Node.Name] = document_state().selection def document_setup(background: Option[Sessions.Background]): Unit = document_state_change(_.copy(session_background = background)) diff -r 872fc664cd99 -r 0ba6f360d38a src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Wed Dec 21 14:14:02 2022 +0100 +++ b/src/Pure/Thy/document_build.scala Wed Dec 21 15:34:33 2022 +0100 @@ -135,12 +135,14 @@ def context( session_context: Export.Session_Context, document_session: Option[Sessions.Base] = None, + document_selection: Document.Node.Name => Boolean = _ => true, progress: Progress = new Progress - ): Context = new Context(session_context, document_session, progress) + ): Context = new Context(session_context, document_session, document_selection, progress) final class Context private[Document_Build]( val session_context: Export.Session_Context, document_session: Option[Sessions.Base], + document_selection: Document.Node.Name => Boolean, val progress: Progress ) { context => @@ -187,8 +189,12 @@ for (name <- all_document_theories) yield { val path = Path.basic(tex_name(name)) - val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true) - val content = YXML.parse_body(entry.text) + val content = + if (document_selection(name)) { + val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true) + YXML.parse_body(entry.text) + } + else Nil File.content(path, content) } diff -r 872fc664cd99 -r 0ba6f360d38a src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Dec 21 14:14:02 2022 +0100 +++ b/src/Pure/Thy/sessions.scala Wed Dec 21 15:34:33 2022 +0100 @@ -112,6 +112,7 @@ infos: List[Info] = Nil ) { def session_name: String = base.session_name + def info: Info = sessions_structure(session_name) def check_errors: Background = if (errors.isEmpty) this diff -r 872fc664cd99 -r 0ba6f360d38a src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Wed Dec 21 14:14:02 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Wed Dec 21 15:34:33 2022 +0100 @@ -176,32 +176,57 @@ } } - private def build_document(): Unit = { - run_process { progress => - show_page(theories_page) - Time.seconds(2.0).sleep() + private def document_build( + session_background: Sessions.Background, + progress: Document_Editor.Log_Progress + ): Unit = { + val store = JEdit_Sessions.sessions_store(PIDE.options.value) + val document_selection = PIDE.editor.document_selection() + + val snapshot = PIDE.session.await_stable_snapshot() + val session_context = + Export.open_session_context(store, session_background, + document_snapshot = Some(snapshot)) + try { + val context = + Document_Build.context(session_context, + 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) } - show_page(log_page) - val res = - Exn.capture { - progress.echo("Start " + Date.now()) - for (i <- 1 to 200) { - progress.echo("message " + i) - Time.seconds(0.1).sleep() - } - progress.echo("Stop " + Date.now()) + // pdf + Bytes.write(Document_Editor.document_output().pdf, doc.pdf) + Document_Editor.view_document() + } + finally { session_context.close() } + } + + private def build_document(): Unit = { + PIDE.editor.document_session() match { + case Some(session_background) if session_background.info.documents.nonEmpty => + run_process { progress => + show_page(log_page) + val res = Exn.capture { document_build(session_background, progress) } + val msg = + res match { + case Exn.Res(_) => Protocol.writeln_message("OK") + case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn)) + } + + finish_process(List(msg)) + + show_state() + show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page) } - val msg = - res match { - case Exn.Res(_) => Protocol.writeln_message("OK") - case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn)) - } - finish_process(List(msg)) - - show_state() - - show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page) - GUI_Thread.later { progress.load() } + case _ => } }