# HG changeset patch
# User wenzelm
# Date 1675447229 -3600
# Node ID 861777e58b7779c387a2b9e5ead8b85e11913181
# Parent  45b9bbe6e3750ab8ffc99b3e845da59ad5e3e231
clarified modules;

diff -r 45b9bbe6e375 -r 861777e58b77 src/Pure/PIDE/document_editor.scala
--- 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)
diff -r 45b9bbe6e375 -r 861777e58b77 src/Tools/jEdit/src/document_dockable.scala
--- 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() }