--- 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 =
--- 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() }