src/Pure/PIDE/document_editor.scala
changeset 77149 3991a35cd740
parent 77147 38077c938d01
child 77161 913c781ff6ba
--- a/src/Pure/PIDE/document_editor.scala	Tue Jan 31 16:13:27 2023 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Tue Jan 31 17:00:33 2023 +0100
@@ -29,6 +29,7 @@
   ) {
     def is_vacuous: Boolean = background.isEmpty
     def is_pending: Boolean = snapshot.isEmpty
+    def is_ready: Boolean = background.isDefined && snapshot.isDefined
 
     def get_background: Sessions.Background = background.get
     def get_variant: Document_Build.Document_Variant = get_background.info.documents.head