# HG changeset patch # User wenzelm # Date 1675453025 -3600 # Node ID 68d8ff34894189a8dd0c30e3c05313f83fe70e68 # Parent 9dc4d9ed886fbcbaeddcd047e6590744a205a5a1 clarified modules; diff -r 9dc4d9ed886f -r 68d8ff348941 src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Fri Feb 03 20:23:37 2023 +0100 +++ b/src/Pure/Thy/document_build.scala Fri Feb 03 20:37:05 2023 +0100 @@ -270,17 +270,6 @@ } - /* build document */ - - def build_document(doc: Document_Variant, verbose: Boolean = false): Document_Output = { - Isabelle_System.with_tmp_dir("document") { tmp_dir => - val engine = get_engine() - val directory = engine.prepare_directory(context, tmp_dir, doc, verbose) - engine.build_document(context, directory, verbose) - } - } - - /* document directory */ def make_directory(dir: Path, doc: Document_Variant): Path = diff -r 9dc4d9ed886f -r 68d8ff348941 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Fri Feb 03 20:23:37 2023 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Fri Feb 03 20:37:05 2023 +0100 @@ -219,9 +219,14 @@ progress = progress) Isabelle_System.make_directory(Document_Editor.document_output_dir()) - val doc = context.build_document(document_session.get_variant, verbose = true) + Isabelle_System.with_tmp_dir("document") { tmp_dir => + val engine = context.get_engine() + val variant = document_session.get_variant + val directory = engine.prepare_directory(context, tmp_dir, variant, verbose = true) + Document_Editor.write_document(document_session.selection, + engine.build_document(context, directory, verbose = true)) + } - Document_Editor.write_document(document_session.selection, doc) Document_Editor.view_document() } finally { session_context.close() }