# HG changeset patch
# User wenzelm
# Date 1547320445 -3600
# Node ID af09cc4792dc34d778883d86019982585882f19a
# Parent  091f57432f057775878297ef6a42a5e496e5290e
more robust: no assumptions about GUI thread or document model;

diff -r 091f57432f05 -r af09cc4792dc src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Jan 12 19:53:57 2019 +0100
+++ b/src/Pure/PIDE/session.scala	Sat Jan 12 20:14:05 2019 +0100
@@ -9,6 +9,7 @@
 
 
 import scala.collection.immutable.Queue
+import scala.annotation.tailrec
 
 
 object Session
@@ -640,6 +641,16 @@
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
     global_state.value.snapshot(name, pending_edits)
 
+  @tailrec final def await_stable_snapshot(): Document.Snapshot =
+  {
+    val snapshot = this.snapshot()
+    if (snapshot.is_outdated) {
+      Thread.sleep(output_delay.ms)
+      await_stable_snapshot()
+    }
+    else snapshot
+  }
+
   def start(start_prover: Prover.Receiver => Prover)
   {
     file_formats
diff -r 091f57432f05 -r af09cc4792dc src/Tools/jEdit/src/isabelle_export.scala
--- a/src/Tools/jEdit/src/isabelle_export.scala	Sat Jan 12 19:53:57 2019 +0100
+++ b/src/Tools/jEdit/src/isabelle_export.scala	Sat Jan 12 20:14:05 2019 +0100
@@ -59,7 +59,7 @@
       explode_url(url, component = component) match {
         case None => null
         case Some(elems) =>
-          val snapshot = PIDE.snapshot()
+          val snapshot = PIDE.session.await_stable_snapshot()
           val version = snapshot.version
           elems match {
             case Nil =>
@@ -96,7 +96,7 @@
       explode_url(url, component = if (ignore_errors) null else component) match {
         case None | Some(Nil) => Bytes.empty.stream()
         case Some(theory :: name_elems) =>
-          val snapshot = PIDE.snapshot()
+          val snapshot = PIDE.session.await_stable_snapshot()
           val version = snapshot.version
           val bytes =
             (for {
@@ -105,6 +105,7 @@
               (_, entry) <- snapshot.state.node_exports(version, node_name).iterator
               if entry.name_elems == name_elems
             } yield entry.uncompressed()).find(_ => true).getOrElse(Bytes.empty)
+
           bytes.stream()
       }
     }