# HG changeset patch
# User wenzelm
# Date 1675453633 -3600
# Node ID 628a34f4f7543cfd816db0d08140026489fcb03a
# Parent  68d8ff34894189a8dd0c30e3c05313f83fe70e68
build only if required, view only after proper build: thus avoid pointless events in "auto build" mode;

diff -r 68d8ff348941 -r 628a34f4f754 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Fri Feb 03 20:37:05 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Fri Feb 03 20:47:13 2023 +0100
@@ -223,11 +223,18 @@
         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))
+        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))
+          Document_Editor.view_document()
+        }
       }
-
-      Document_Editor.view_document()
     }
     finally { session_context.close() }
   }