build only if required, view only after proper build: thus avoid pointless events in "auto build" mode;
authorwenzelm
Fri, 03 Feb 2023 20:47:13 +0100
changeset 77187 628a34f4f754
parent 77186 68d8ff348941
child 77188 608668d39689
build only if required, view only after proper build: thus avoid pointless events in "auto build" mode;
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() }
   }