--- a/src/Pure/PIDE/document_editor.scala Mon Dec 19 15:29:24 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala Tue Dec 20 13:59:07 2022 +0100
@@ -46,10 +46,36 @@
sealed case class State(
session_background: Option[Sessions.Background] = None,
+ selection: Set[Document.Node.Name] = Set.empty,
views: Set[AnyRef] = Set.empty,
) {
def is_active: Boolean = session_background.isDefined && views.nonEmpty
+ def is_required(name: Document.Node.Name): Boolean =
+ is_active && selection.contains(name) && all_document_theories.contains(name)
+
+ def required: List[Document.Node.Name] =
+ if (is_active) all_document_theories.filter(selection) else Nil
+
+ def all_document_theories: List[Document.Node.Name] =
+ session_background match {
+ case Some(background) => background.base.all_document_theories
+ case None => Nil
+ }
+
+ def select(
+ names: Iterable[Document.Node.Name],
+ set: Boolean = false,
+ toggle: Boolean = false
+ ): State = {
+ copy(selection =
+ names.foldLeft(selection) {
+ case (sel, name) =>
+ val b = if (toggle) !selection(name) else set
+ if (b) sel + name else sel - name
+ })
+ }
+
def register_view(id: AnyRef): State = copy(views = views + id)
def unregister_view(id: AnyRef): State = copy(views = views - id)
}