# HG changeset patch
# User wenzelm
# Date 1660316310 -7200
# Node ID d298da61655af5151de6cac07ff680037eaaf9cb
# Parent  ad00fbf64bff587e07b0528ff3cd76bf85b2e632
clarified signature --- more operations;

diff -r ad00fbf64bff -r d298da61655a src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Fri Aug 12 16:08:12 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Fri Aug 12 16:58:30 2022 +0200
@@ -128,6 +128,9 @@
     document_session: Option[Sessions.Base],
     val progress: Progress = new Progress
   ) {
+    context =>
+
+
     /* session info */
 
     private val base = document_session getOrElse session_context.session_base
@@ -201,6 +204,17 @@
     }
 
 
+    /* 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)
+        engine.build_document(context, directory, verbose)
+      }
+    }
+
+
     /* document directory */
 
     def prepare_directory(