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