--- a/src/Pure/PIDE/document_editor.scala Fri Feb 03 16:50:14 2023 +0100
+++ b/src/Pure/PIDE/document_editor.scala Fri Feb 03 19:00:29 2023 +0100
@@ -14,6 +14,12 @@
def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output")
def document_output(): Path = document_output_dir() + Path.basic(document_name)
+ def write_document(doc: Document_Build.Document_Output): Unit = {
+ val output = document_output()
+ File.write(output.log, doc.log)
+ Bytes.write(output.pdf, doc.pdf)
+ }
+
def view_document(): Unit = {
val path = document_output().pdf
if (path.is_file) Isabelle_System.pdf_viewer(path)
--- a/src/Tools/jEdit/src/document_dockable.scala Fri Feb 03 16:50:14 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Fri Feb 03 19:00:29 2023 +0100
@@ -221,8 +221,7 @@
Isabelle_System.make_directory(Document_Editor.document_output_dir())
val doc = context.build_document(document_session.get_variant, verbose = true)
- File.write(Document_Editor.document_output().log, doc.log)
- Bytes.write(Document_Editor.document_output().pdf, doc.pdf)
+ Document_Editor.write_document(doc)
Document_Editor.view_document()
}
finally { session_context.close() }