clarified signature --- more operations;
authorwenzelm
Fri, 12 Aug 2022 16:58:30 +0200
changeset 75826 d298da61655a
parent 75825 ad00fbf64bff
child 75827 4920ebbde486
clarified signature --- more operations;
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(