| changeset 76716 | a7602257a825 |
| parent 76715 | bf5ff407f32f |
| child 76730 | 1b8dd8c0492f |
--- a/src/Pure/PIDE/document_editor.scala Tue Dec 20 13:59:07 2022 +0100 +++ b/src/Pure/PIDE/document_editor.scala Tue Dec 20 16:34:13 2022 +0100 @@ -63,6 +63,9 @@ case None => Nil } + def active_document_theories: List[Document.Node.Name] = + if (is_active) all_document_theories else Nil + def select( names: Iterable[Document.Node.Name], set: Boolean = false,