| 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