# HG changeset patch
# User wenzelm
# Date 1675164420 -3600
# Node ID 42c3970e1ac13b94f25c8396540ea2c0cb9b2398
# Parent  61f6bb753cbf5c0c0fa60465238299023b55552a
clarified Document_Editor.Session: more explicit types, more robust operations;
eliminated await_stable_snapshot in favour of delay_build;

diff -r 61f6bb753cbf -r 42c3970e1ac1 src/Pure/PIDE/document_editor.scala
--- a/src/Pure/PIDE/document_editor.scala	Mon Jan 30 16:26:10 2023 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Tue Jan 31 12:27:00 2023 +0100
@@ -22,6 +22,19 @@
 
   /* configuration state */
 
+  sealed case class Session(
+    background: Option[Sessions.Background],
+    selection: Set[Document.Node.Name],
+    snapshot: Option[Document.Snapshot]
+  ) {
+    def is_vacuous: Boolean = background.isEmpty
+    def is_pending: Boolean = snapshot.isEmpty
+
+    def get_background: Sessions.Background = background.get
+    def get_variant: Document_Build.Document_Variant = get_background.info.documents.head
+    def get_snapshot: Document.Snapshot = snapshot.get
+  }
+
   sealed case class State(
     session_background: Option[Sessions.Background] = None,
     selection: Set[Document.Node.Name] = Set.empty,
@@ -53,5 +66,16 @@
 
     def register_view(id: AnyRef): State = copy(views = views + id)
     def unregister_view(id: AnyRef): State = copy(views = views - id)
+
+    def session(get_snapshot: () => Document.Snapshot): Session = {
+      val background = session_background.filter(_.info.documents.nonEmpty)
+      val snapshot =
+        if (background.isEmpty) None
+        else {
+          val snapshot = get_snapshot()
+          if (snapshot.is_outdated) None else Some(snapshot)
+        }
+      Session(background, selection, snapshot)
+    }
   }
 }
diff -r 61f6bb753cbf -r 42c3970e1ac1 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Jan 30 16:26:10 2023 +0100
+++ b/src/Pure/PIDE/editor.scala	Tue Jan 31 12:27:00 2023 +0100
@@ -37,8 +37,8 @@
     if (changed) document_state_changed()
   }
 
-  def document_session(): Option[Sessions.Background] =
-    document_state().session_background.filter(_.info.documents.nonEmpty)
+  def document_session(): Document_Editor.Session =
+    document_state().session(() => session.snapshot())
 
   def document_required(): List[Document.Node.Name] = {
     val st = document_state()
diff -r 61f6bb753cbf -r 42c3970e1ac1 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Mon Jan 30 16:26:10 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 12:27:00 2023 +0100
@@ -197,24 +197,21 @@
   }
 
   private def document_build(
-    session_background: Sessions.Background,
+    document_session: Document_Editor.Session,
     progress: Log_Progress
   ): Unit = {
-    val document_selection = PIDE.editor.document_selection()
-
-    val snapshot = PIDE.session.await_stable_snapshot()
+    val session_background = document_session.get_background
+    val snapshot = document_session.get_snapshot
     val session_context = JEdit_Sessions.open_session_context(document_snapshot = Some(snapshot))
     try {
       val context =
         Document_Build.context(session_context,
           document_session = Some(session_background.base),
-          document_selection = document_selection,
+          document_selection = document_session.selection,
           progress = progress)
 
-      val variant = session_background.info.documents.head
-
       Isabelle_System.make_directory(Document_Editor.document_output_dir())
-      val doc = context.build_document(variant, verbose = true)
+      val doc = context.build_document(document_session.get_variant, verbose = true)
 
       File.write(Document_Editor.document_output().log, doc.log)
       Bytes.write(Document_Editor.document_output().pdf, doc.pdf)
@@ -223,33 +220,40 @@
     finally { session_context.close() }
   }
 
-  private def build_document(): Unit = {
-    PIDE.editor.document_session() match {
-      case Some(session_background) =>
-        run_process(only_running = true) { progress =>
-          show_page(output_page)
-          val result = Exn.capture { document_build(session_background, progress) }
-          val msgs =
-            result match {
-              case Exn.Res(_) =>
-                List(Protocol.writeln_message("OK"))
-              case Exn.Exn(exn: Document_Build.Build_Error) =>
-                exn.log_errors.map(s => Protocol.error_message(YXML.parse_body(s)))
-              case Exn.Exn(exn) =>
-                List(Protocol.error_message(YXML.parse_body(Exn.print(exn))))
-            }
+  private def document_build_attempt(): Boolean = {
+    val document_session = PIDE.editor.document_session()
+    if (document_session.is_vacuous) true
+    else if (document_session.is_pending) false
+    else {
+      run_process(only_running = true) { progress =>
+        show_page(output_page)
+        val result = Exn.capture { document_build(document_session, progress) }
+        val msgs =
+          result match {
+            case Exn.Res(_) =>
+              List(Protocol.writeln_message("OK"))
+            case Exn.Exn(exn: Document_Build.Build_Error) =>
+              exn.log_errors.map(s => Protocol.error_message(YXML.parse_body(s)))
+            case Exn.Exn(exn) =>
+              List(Protocol.error_message(YXML.parse_body(Exn.print(exn))))
+          }
 
-          progress.stop_program()
-          running_process(progress)
-          finish_process(Pretty.separate(msgs))
+        progress.stop_program()
+        running_process(progress)
+        finish_process(Pretty.separate(msgs))
 
-          show_state()
-          show_page(if (Exn.is_interrupt_exn(result)) input_page else output_page)
-        }
-      case None =>
+        show_state()
+        show_page(if (Exn.is_interrupt_exn(result)) input_page else output_page)
+      }
+      true
     }
   }
 
+  private lazy val delay_build: Delay =
+    Delay.first(PIDE.session.output_delay, gui = true) {
+      if (!document_build_attempt()) delay_build.invoke()
+    }
+
 
   /* controls */
 
@@ -274,7 +278,7 @@
   private val build_button =
     new GUI.Button("<html><b>Build</b></html>") {
       tooltip = "Build document"
-      override def clicked(): Unit = build_document()
+      override def clicked(): Unit = delay_build.invoke()
     }
 
   private val cancel_button =