# HG changeset patch # User wenzelm # Date 1671541147 -3600 # Node ID bf5ff407f32f4cb98e9947795419f31f16013e7d # Parent 95a926d483c54362f9e419833f114f1da5521dab clarified state of document model vs. document editor selection (again, see also a9d52d02bd83); diff -r 95a926d483c5 -r bf5ff407f32f src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon Dec 19 15:29:24 2022 +0100 +++ b/src/Pure/PIDE/document.scala Tue Dec 20 13:59:07 2022 +0100 @@ -760,7 +760,6 @@ def get_text(range: Text.Range): Option[String] - def get_required(document: Boolean): Boolean def node_required: Boolean def get_blob: Option[Blob] diff -r 95a926d483c5 -r bf5ff407f32f src/Pure/PIDE/document_editor.scala --- 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) } diff -r 95a926d483c5 -r bf5ff407f32f src/Pure/PIDE/editor.scala --- a/src/Pure/PIDE/editor.scala Mon Dec 19 15:29:24 2022 +0100 +++ b/src/Pure/PIDE/editor.scala Tue Dec 20 13:59:07 2022 +0100 @@ -20,21 +20,33 @@ protected val document_editor: Synchronized[Document_Editor.State] = Synchronized(Document_Editor.State()) - def document_session: Option[Sessions.Background] = document_editor.value.session_background - def document_active: Boolean = document_editor.value.is_active - def document_active_changed(): Unit = {} - private def document_editor_change(f: Document_Editor.State => Document_Editor.State): Unit = { + protected def document_state(): Document_Editor.State = document_editor.value + + protected def document_state_changed(): Unit = {} + private def document_state_change(f: Document_Editor.State => Document_Editor.State): Unit = { val changed = document_editor.change_result { st => val st1 = f(st) - (st.is_active != st1.is_active, st1) + (st.required != st1.required, st1) } - if (changed) document_active_changed() + if (changed) document_state_changed() } + + def document_session(): Option[Sessions.Background] = document_state().session_background + def document_required(): List[Document.Node.Name] = document_state().required + def document_node_required(name: Document.Node.Name): Boolean = document_state().is_required(name) + def document_setup(background: Option[Sessions.Background]): Unit = - document_editor_change(_.copy(session_background = background)) - def document_init(id: AnyRef): Unit = document_editor_change(_.register_view(id)) - def document_exit(id: AnyRef): Unit = document_editor_change(_.unregister_view(id)) + document_state_change(_.copy(session_background = background)) + + def document_select( + names: Iterable[Document.Node.Name], + set: Boolean = false, + toggle: Boolean = false + ): Unit = document_state_change(_.select(names, set = set, toggle = toggle)) + + def document_init(id: AnyRef): Unit = document_state_change(_.register_view(id)) + def document_exit(id: AnyRef): Unit = document_state_change(_.unregister_view(id)) /* current situation */ diff -r 95a926d483c5 -r bf5ff407f32f src/Tools/VSCode/src/vscode_model.scala --- a/src/Tools/VSCode/src/vscode_model.scala Mon Dec 19 15:29:24 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_model.scala Tue Dec 20 13:59:07 2022 +0100 @@ -59,7 +59,7 @@ node_name: Document.Node.Name ): VSCode_Model = { VSCode_Model(session, editor, node_name, Content.empty, - theory_required = File_Format.registry.is_theory(node_name)) + node_required = File_Format.registry.is_theory(node_name)) } } @@ -70,8 +70,7 @@ content: VSCode_Model.Content, version: Option[Long] = None, external_file: Boolean = false, - theory_required: Boolean = false, - document_required: Boolean = false, + node_required: Boolean = false, last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty, pending_edits: List[Text.Edit] = Nil, published_diagnostics: List[Text.Info[Command.Results]] = Nil, @@ -79,14 +78,6 @@ ) extends Document.Model { model => - /* required */ - - def get_required(document: Boolean): Boolean = - if (document) document_required else theory_required - - def node_required: Boolean = get_required(false) - - /* content */ def get_text(range: Text.Range): Option[String] = content.doc.get_text(range) @@ -117,6 +108,8 @@ if (is_theory) { val snapshot = model.snapshot() + val required = node_required || editor.document_node_required(node_name) + val caret_perspective = resources.options.int("vscode_caret_perspective") max 0 val caret_range = if (caret_perspective != 0) { @@ -144,7 +137,7 @@ val overlays = editor.node_overlays(node_name) (snapshot.node.load_commands_changed(doc_blobs), - Document.Node.Perspective(node_required, text_perspective, overlays)) + Document.Node.Perspective(required, text_perspective, overlays)) } else (false, Document.Node.Perspective_Text.empty) } diff -r 95a926d483c5 -r bf5ff407f32f src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Mon Dec 19 15:29:24 2022 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Tue Dec 20 13:59:07 2022 +0100 @@ -182,15 +182,14 @@ /* required nodes */ - def required_nodes(document: Boolean): Set[Document.Node.Name] = + def nodes_required(): Set[Document.Node.Name] = (for { (node_name, model) <- state.value.models.iterator - if model.get_required(document) + if model.node_required } yield node_name).toSet def node_required( name: Document.Node.Name, - document: Boolean = false, toggle: Boolean = false, set: Boolean = false ) : Unit = { @@ -201,13 +200,13 @@ st.models.get(name) match { case None => (false, st) case Some(model) => - val a = model.get_required(document) + val a = model.node_required val b = if (toggle) !a else set model match { case m: File_Model if a != b => - (true, st.copy(models = st.models + (name -> m.set_required(document, b)))) + (true, st.copy(models = st.models + (name -> m.set_node_required(b)))) case m: Buffer_Model if a != b => - m.set_required(document, b); (true, st) + m.set_node_required(b); (true, st) case _ => (false, st) } }) @@ -216,12 +215,11 @@ def view_node_required( view: View, - document: Boolean = false, toggle: Boolean = false, set: Boolean = false ): Unit = Document_Model.get(view.getBuffer).foreach(model => - node_required(model.node_name, document = document, toggle = toggle, set = set)) + node_required(model.node_name, toggle = toggle, set = set)) /* flushed edits */ @@ -334,9 +332,6 @@ def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil - def node_required: Boolean = - get_required(false) || PIDE.editor.document_active && get_required(true) - def node_perspective( doc_blobs: Document.Blobs, hidden: Boolean @@ -346,6 +341,8 @@ if (JEdit_Options.continuous_checking() && is_theory) { val snapshot = this.snapshot() + val required = node_required || PIDE.editor.document_node_required(node_name) + val reparse = snapshot.node.load_commands_changed(doc_blobs) val perspective = if (hidden) Text.Perspective.empty @@ -356,7 +353,7 @@ } val overlays = PIDE.editor.node_overlays(node_name) - (reparse, Document.Node.Perspective(node_required, perspective, overlays)) + (reparse, Document.Node.Perspective(required, perspective, overlays)) } else (false, Document.Node.Perspective_Text.empty) } @@ -377,13 +374,12 @@ object File_Model { def empty(session: Session): File_Model = File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""), - false, false, Document.Node.Perspective_Text.empty, Nil) + false, Document.Node.Perspective_Text.empty, Nil) def init(session: Session, node_name: Document.Node.Name, text: String, - theory_required: Boolean = false, - document_required: Boolean = false, + node_required: Boolean = false, last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty, pending_edits: List[Text.Edit] = Nil ): File_Model = { @@ -391,9 +387,8 @@ file.foreach(PIDE.plugin.file_watcher.register_parent(_)) val content = Document_Model.File_Content(text) - val theory_required1 = theory_required || File_Format.registry.is_theory(node_name) - File_Model(session, node_name, file, content, theory_required1, document_required, - last_perspective, pending_edits) + val node_required1 = node_required || File_Format.registry.is_theory(node_name) + File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits) } } @@ -402,18 +397,13 @@ node_name: Document.Node.Name, file: Option[JFile], content: Document_Model.File_Content, - theory_required: Boolean, - document_required: Boolean, + node_required: Boolean, last_perspective: Document.Node.Perspective_Text.T, pending_edits: List[Text.Edit] ) extends Document_Model { /* required */ - def get_required(document: Boolean): Boolean = - if (document) document_required else theory_required - - def set_required(document: Boolean, b: Boolean): File_Model = - if (document) copy(document_required = b) else copy(theory_required = b) + def set_node_required(b: Boolean): File_Model = copy(node_required = b) /* text */ @@ -505,13 +495,9 @@ /* perspective */ // owned by GUI thread - private var _theory_required = false - private var _document_required = false - - def get_required(document: Boolean): Boolean = - if (document) _document_required else _theory_required - def set_required(document: Boolean, b: Boolean): Unit = - GUI_Thread.require { if (document) _document_required = b else _theory_required = b } + private var _node_required = false + def node_required: Boolean = _node_required + def set_node_required(b: Boolean): Unit = GUI_Thread.require { _node_required = b } def document_view_iterator: Iterator[Document_View] = for { @@ -683,8 +669,7 @@ case None => pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))) case Some(file_model) => - set_required(false, file_model.theory_required) - set_required(true, file_model.document_required) + set_node_required(file_model.node_required) pending_edits.set_last_perspective(file_model.last_perspective) pending_edits.edit( file_model.pending_edits ::: @@ -707,8 +692,7 @@ init_token_marker() File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), - theory_required = _theory_required, - document_required = _document_required, + node_required = _node_required, last_perspective = pending_edits.get_last_perspective, pending_edits = pending_edits.get_edits) } diff -r 95a926d483c5 -r bf5ff407f32f src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Mon Dec 19 15:29:24 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Dec 20 13:59:07 2022 +0100 @@ -61,7 +61,7 @@ session.global_options.post(Session.Global_Options(PIDE.options.value)) } - override def document_active_changed(): Unit = state_changed() + override def document_state_changed(): Unit = state_changed() /* current situation */ diff -r 95a926d483c5 -r bf5ff407f32f src/Tools/jEdit/src/theories_status.scala --- a/src/Tools/jEdit/src/theories_status.scala Mon Dec 19 15:29:24 2022 +0100 +++ b/src/Tools/jEdit/src/theories_status.scala Tue Dec 20 13:59:07 2022 +0100 @@ -28,8 +28,8 @@ private var document_required = Set.empty[Document.Node.Name] private def init_state(): Unit = GUI_Thread.require { - theory_required = Document_Model.required_nodes(false) - document_required = Document_Model.required_nodes(true) + theory_required = Document_Model.nodes_required() + document_required = PIDE.editor.document_required().toSet } @@ -156,8 +156,8 @@ component.label_border(name) component.label.text = name.theory_base_name + - (if (!document && PIDE.editor.document_active && document_required.contains(name)) - document_marker else no_document_marker) + (if (!document && PIDE.editor.document_node_required(name)) document_marker + else no_document_marker) component } } @@ -183,7 +183,9 @@ val index_location = peer.indexToLocation(index) if (node_renderer.in_required(index_location, point)) { if (clicks == 1) { - Document_Model.node_required(listData(index), toggle = true, document = document) + val name = listData(index) + if (document) PIDE.editor.document_select(Set(name), toggle = true) + else Document_Model.node_required(name, toggle = true) } } else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node)