src/Tools/jEdit/src/document_model.scala
changeset 73959 7202e12cb324
parent 73774 c42144d9dde6
child 74263 6b213c0115f5
equal deleted inserted replaced
73958:d83e7e444b43 73959:7202e12cb324
   368 
   368 
   369   @tailrec final def await_stable_snapshot(): Document.Snapshot =
   369   @tailrec final def await_stable_snapshot(): Document.Snapshot =
   370   {
   370   {
   371     val snapshot = this.snapshot()
   371     val snapshot = this.snapshot()
   372     if (snapshot.is_outdated) {
   372     if (snapshot.is_outdated) {
   373       PIDE.options.seconds("editor_output_delay").sleep
   373       PIDE.options.seconds("editor_output_delay").sleep()
   374       await_stable_snapshot()
   374       await_stable_snapshot()
   375     }
   375     }
   376     else snapshot
   376     else snapshot
   377   }
   377   }
   378 }
   378 }