# HG changeset patch
# User wenzelm
# Date 1675605590 -3600
# Node ID e312c7fa3bad8dda893e5dc521b88f68223dc689
# Parent  7438d516ab4f2d71f401e4677e757136b97c1389
clarified modules;

diff -r 7438d516ab4f -r e312c7fa3bad src/Pure/PIDE/document_editor.scala
--- a/src/Pure/PIDE/document_editor.scala	Sun Feb 05 14:57:14 2023 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Sun Feb 05 14:59:50 2023 +0100
@@ -146,4 +146,37 @@
       Session(background, selection, snapshot)
     }
   }
+
+
+  /* build */
+
+  def build(
+    session_context: Export.Session_Context,
+    document_session: Document_Editor.Session,
+    progress: Progress
+  ): Unit = {
+    val session_background = document_session.get_background
+    val context =
+      Document_Build.context(session_context,
+        document_session = Some(session_background.base),
+        document_selection = document_session.selection,
+        progress = progress)
+
+    Isabelle_System.make_directory(document_output_dir())
+    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)
+      val ok =
+        Meta_Data.read() match {
+          case Some(meta_data) =>
+            meta_data.check_files() && meta_data.sources == directory.sources
+          case None => false
+        }
+      if (!ok) {
+        write_document(document_session.selection,
+          engine.build_document(context, directory, verbose = true))
+      }
+    }
+  }
 }
diff -r 7438d516ab4f -r e312c7fa3bad src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Sun Feb 05 14:57:14 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Sun Feb 05 14:59:50 2023 +0100
@@ -204,36 +204,6 @@
     }
   }
 
-  private def document_build(
-    session_context: Export.Session_Context,
-    document_session: Document_Editor.Session,
-    progress: Progress
-  ): Unit = {
-    val session_background = document_session.get_background
-    val context =
-      Document_Build.context(session_context,
-        document_session = Some(session_background.base),
-        document_selection = document_session.selection,
-        progress = progress)
-
-    Isabelle_System.make_directory(Document_Editor.document_output_dir())
-    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)
-      val ok =
-        Document_Editor.Meta_Data.read() match {
-          case Some(meta_data) =>
-            meta_data.check_files() && meta_data.sources == directory.sources
-          case None => false
-        }
-      if (!ok) {
-        Document_Editor.write_document(document_session.selection,
-          engine.build_document(context, directory, verbose = true))
-      }
-    }
-  }
-
   private def document_build_attempt(): Boolean = {
     val document_session = PIDE.editor.document_session()
     if (document_session.is_vacuous) true
@@ -246,7 +216,7 @@
         val result = Exn.capture {
           val snapshot = document_session.get_snapshot
           using(JEdit_Sessions.open_session_context(document_snapshot = Some(snapshot))) {
-            session_context => document_build(session_context, document_session, progress)
+            session_context => Document_Editor.build(session_context, document_session, progress)
           }
         }
         val msgs =