more robust: no assumptions about GUI thread or document model;
authorwenzelm
Sat Jan 12 20:14:05 2019 +0100 (10 months ago)
changeset 69640af09cc4792dc
parent 69639 091f57432f05
child 69641 fc2b565fa377
more robust: no assumptions about GUI thread or document model;
src/Pure/PIDE/session.scala
src/Tools/jEdit/src/isabelle_export.scala
     1.1 --- a/src/Pure/PIDE/session.scala	Sat Jan 12 19:53:57 2019 +0100
     1.2 +++ b/src/Pure/PIDE/session.scala	Sat Jan 12 20:14:05 2019 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4  
     1.5  
     1.6  import scala.collection.immutable.Queue
     1.7 +import scala.annotation.tailrec
     1.8  
     1.9  
    1.10  object Session
    1.11 @@ -640,6 +641,16 @@
    1.12        pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
    1.13      global_state.value.snapshot(name, pending_edits)
    1.14  
    1.15 +  @tailrec final def await_stable_snapshot(): Document.Snapshot =
    1.16 +  {
    1.17 +    val snapshot = this.snapshot()
    1.18 +    if (snapshot.is_outdated) {
    1.19 +      Thread.sleep(output_delay.ms)
    1.20 +      await_stable_snapshot()
    1.21 +    }
    1.22 +    else snapshot
    1.23 +  }
    1.24 +
    1.25    def start(start_prover: Prover.Receiver => Prover)
    1.26    {
    1.27      file_formats
     2.1 --- a/src/Tools/jEdit/src/isabelle_export.scala	Sat Jan 12 19:53:57 2019 +0100
     2.2 +++ b/src/Tools/jEdit/src/isabelle_export.scala	Sat Jan 12 20:14:05 2019 +0100
     2.3 @@ -59,7 +59,7 @@
     2.4        explode_url(url, component = component) match {
     2.5          case None => null
     2.6          case Some(elems) =>
     2.7 -          val snapshot = PIDE.snapshot()
     2.8 +          val snapshot = PIDE.session.await_stable_snapshot()
     2.9            val version = snapshot.version
    2.10            elems match {
    2.11              case Nil =>
    2.12 @@ -96,7 +96,7 @@
    2.13        explode_url(url, component = if (ignore_errors) null else component) match {
    2.14          case None | Some(Nil) => Bytes.empty.stream()
    2.15          case Some(theory :: name_elems) =>
    2.16 -          val snapshot = PIDE.snapshot()
    2.17 +          val snapshot = PIDE.session.await_stable_snapshot()
    2.18            val version = snapshot.version
    2.19            val bytes =
    2.20              (for {
    2.21 @@ -105,6 +105,7 @@
    2.22                (_, entry) <- snapshot.state.node_exports(version, node_name).iterator
    2.23                if entry.name_elems == name_elems
    2.24              } yield entry.uncompressed()).find(_ => true).getOrElse(Bytes.empty)
    2.25 +
    2.26            bytes.stream()
    2.27        }
    2.28      }