--- 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
--- 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()
}
}