# HG changeset patch
# User wenzelm
# Date 1667853129 -3600
# Node ID a9d52d02bd8312ff401eef5167a34c7fabe8fd90
# Parent  5ba13c82a286403f98f8b2333f5345bb6199e17b
clarified node_required status: distinguish theory_required vs. document_required;
more robust and more correct Geometry.in operation;

diff -r 5ba13c82a286 -r a9d52d02bd83 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Nov 06 23:10:28 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Nov 07 21:32:09 2022 +0100
@@ -761,7 +761,9 @@
 
     def get_text(range: Text.Range): Option[String]
 
-    def node_required: Boolean
+    def get_required(document: Boolean): Boolean
+    def node_required: Boolean = get_required(false) || get_required(true)
+
     def get_blob: Option[Blob]
     def bibtex_entries: List[Text.Info[String]]
 
diff -r 5ba13c82a286 -r a9d52d02bd83 src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Sun Nov 06 23:10:28 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Mon Nov 07 21:32:09 2022 +0100
@@ -59,7 +59,7 @@
     node_name: Document.Node.Name
   ): VSCode_Model = {
     VSCode_Model(session, editor, node_name, Content.empty,
-      node_required = File_Format.registry.is_theory(node_name))
+      theory_required = File_Format.registry.is_theory(node_name))
   }
 }
 
@@ -70,7 +70,8 @@
   content: VSCode_Model.Content,
   version: Option[Long] = None,
   external_file: Boolean = false,
-  node_required: Boolean = false,
+  theory_required: Boolean = false,
+  document_required: Boolean = false,
   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
   pending_edits: List[Text.Edit] = Nil,
   published_diagnostics: List[Text.Info[Command.Results]] = Nil,
@@ -78,6 +79,11 @@
 ) extends Document.Model {
   model =>
 
+  /* required */
+
+  def get_required(document: Boolean): Boolean =
+    if (document) document_required else theory_required
+
 
   /* content */
 
diff -r 5ba13c82a286 -r a9d52d02bd83 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Nov 06 23:10:28 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Nov 07 21:32:09 2022 +0100
@@ -182,14 +182,15 @@
 
   /* required nodes */
 
-  def required_nodes(): Set[Document.Node.Name] =
+  def required_nodes(document: Boolean): Set[Document.Node.Name] =
     (for {
       (node_name, model) <- state.value.models.iterator
-      if model.node_required
+      if model.get_required(document)
     } yield node_name).toSet
 
   def node_required(
     name: Document.Node.Name,
+    document: Boolean = false,
     toggle: Boolean = false,
     set: Boolean = false
   ) : Unit = {
@@ -200,12 +201,13 @@
         st.models.get(name) match {
           case None => (false, st)
           case Some(model) =>
-            val required = if (toggle) !model.node_required else set
+            val a = model.get_required(document)
+            val b = if (toggle) !a else set
             model match {
-              case model1: File_Model if required != model1.node_required =>
-                (true, st.copy(models = st.models + (name -> model1.copy(node_required = required))))
-              case model1: Buffer_Model if required != model1.node_required =>
-                model1.set_node_required(required); (true, st)
+              case m: File_Model if a != b =>
+                (true, st.copy(models = st.models + (name -> m.set_required(document, b))))
+              case m: Buffer_Model if a != b =>
+                m.set_required(document, b); (true, st)
               case _ => (false, st)
             }
         })
@@ -215,9 +217,14 @@
     }
   }
 
-  def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit =
+  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, toggle = toggle, set = set))
+      node_required(model.node_name, document = document, toggle = toggle, set = set))
 
 
   /* flushed edits */
@@ -370,12 +377,13 @@
 object File_Model {
   def empty(session: Session): File_Model =
     File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
-      false, Document.Node.no_perspective_text, Nil)
+      false, false, Document.Node.no_perspective_text, Nil)
 
   def init(session: Session,
     node_name: Document.Node.Name,
     text: String,
-    node_required: Boolean = false,
+    theory_required: Boolean = false,
+    document_required: Boolean = false,
     last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
     pending_edits: List[Text.Edit] = Nil
   ): File_Model = {
@@ -383,8 +391,9 @@
     file.foreach(PIDE.plugin.file_watcher.register_parent(_))
 
     val content = Document_Model.File_Content(text)
-    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)
+    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)
   }
 }
 
@@ -393,10 +402,20 @@
   node_name: Document.Node.Name,
   file: Option[JFile],
   content: Document_Model.File_Content,
-  node_required: Boolean,
+  theory_required: Boolean,
+  document_required: Boolean,
   last_perspective: Document.Node.Perspective_Text,
   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)
+
+
   /* text */
 
   def get_text(range: Text.Range): Option[String] =
@@ -486,9 +505,13 @@
   /* perspective */
 
   // owned by GUI thread
-  private var _node_required = false
-  def node_required: Boolean = _node_required
-  def set_node_required(b: Boolean): Unit = GUI_Thread.require { _node_required = b }
+  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 }
 
   def document_view_iterator: Iterator[Document_View] =
     for {
@@ -660,7 +683,8 @@
       case None =>
         pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
       case Some(file_model) =>
-        set_node_required(file_model.node_required)
+        set_required(false, file_model.theory_required)
+        set_required(true, file_model.document_required)
         pending_edits.set_last_perspective(file_model.last_perspective)
         pending_edits.edit(
           file_model.pending_edits :::
@@ -682,7 +706,10 @@
     buffer.removeBufferListener(buffer_listener)
     init_token_marker()
 
-    File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required,
-      pending_edits.get_last_perspective, pending_edits.get_edits)
+    File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer),
+      theory_required = _theory_required,
+      document_required = _document_required,
+      last_perspective = pending_edits.get_last_perspective,
+      pending_edits = pending_edits.get_edits)
   }
 }
diff -r 5ba13c82a286 -r a9d52d02bd83 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sun Nov 06 23:10:28 2022 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Nov 07 21:32:09 2022 +0100
@@ -35,17 +35,26 @@
       case MouseClicked(_, point, _, clicks, _) =>
         val index = peer.locationToIndex(point)
         if (index >= 0) {
-          if (in_checkbox(peer.indexToLocation(index), point)) {
-            if (clicks == 1) Document_Model.node_required(listData(index), toggle = true)
+          val index_location = peer.indexToLocation(index)
+          val a = in_required(index_location, point)
+          val b = in_required(index_location, point, document = true)
+          if (a || b) {
+            if (clicks == 1) {
+              Document_Model.node_required(listData(index), toggle = true, document = b)
+            }
           }
           else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node)
         }
       case MouseMoved(_, point, _) =>
         val index = peer.locationToIndex(point)
         val index_location = peer.indexToLocation(index)
-        if (index >= 0 && in_checkbox(index_location, point)) {
+        if (index >= 0 && in_required(index_location, point)) {
           tooltip = "Mark as required for continuous checking"
-        } else if (index >= 0 && in_label(index_location, point)) {
+        }
+        else if (index >= 0 && in_required(index_location, point, document = true)) {
+          tooltip = "Mark as required for continuous checking, with inclusion in document"
+        }
+        else if (index >= 0 && in_label(index_location, point)) {
           val name = listData(index)
           val st = nodes_status.overall_node_status(name)
           tooltip =
@@ -94,17 +103,20 @@
   /* component state -- owned by GUI thread */
 
   private var nodes_status = Document_Status.Nodes_Status.empty
-  private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
+  private var theory_required: Set[Document.Node.Name] = Document_Model.required_nodes(false)
+  private var document_required: Set[Document.Node.Name] = Document_Model.required_nodes(true)
 
   private class Geometry {
     private var location: Point = null
     private var size: Dimension = null
 
-    def in(location0: Point, p: Point): Boolean = {
-      location != null && size != null &&
-        location0.x + location.x <= p.x && p.x < location0.x + size.width &&
-        location0.y + location.y <= p.y && p.y < location0.y + size.height
-    }
+    def in(location0: Point, p: Point): Boolean =
+      location != null && size != null && location0 != null && p != null && {
+        val x = location0.x + location.x
+        val y = location0.y + location.y
+        x <= p.x && p.x < x + size.width &&
+        y <= p.y && p.y < y + size.height
+      }
 
     def update(new_location: Point, new_size: Dimension): Unit = {
       if (new_location != null && new_size != null) {
@@ -114,12 +126,25 @@
     }
   }
 
-  private def in_checkbox(location0: Point, p: Point): Boolean =
-    Node_Renderer_Component != null && Node_Renderer_Component.checkbox_geometry.in(location0, p)
+  private def in_required(location0: Point, p: Point, document: Boolean = false): Boolean =
+    Node_Renderer_Component != null && {
+      val required =
+        if (document) Node_Renderer_Component.document_required
+        else Node_Renderer_Component.theory_required
+      required.geometry.in(location0, p)
+    }
 
   private def in_label(location0: Point, p: Point): Boolean =
     Node_Renderer_Component != null && Node_Renderer_Component.label_geometry.in(location0, p)
 
+  private class Required extends CheckBox {
+    val geometry = new Geometry
+    opaque = false
+    override def paintComponent(gfx: Graphics2D): Unit = {
+      super.paintComponent(gfx)
+      geometry.update(location, size)
+    }
+  }
 
   private object Node_Renderer_Component extends BorderPanel {
     opaque = true
@@ -127,14 +152,8 @@
 
     var node_name: Document.Node.Name = Document.Node.Name.empty
 
-    val checkbox_geometry = new Geometry
-    val checkbox: CheckBox = new CheckBox {
-      opaque = false
-      override def paintComponent(gfx: Graphics2D): Unit = {
-        super.paintComponent(gfx)
-        checkbox_geometry.update(location, size)
-      }
-    }
+    val theory_required = new Required
+    val document_required = new Required
 
     val label_geometry = new Geometry
     val label: Label = new Label {
@@ -195,8 +214,9 @@
           BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2))
     }
 
-    layout(checkbox) = BorderPanel.Position.West
+    layout(theory_required) = BorderPanel.Position.West
     layout(label) = BorderPanel.Position.Center
+    layout(document_required) = BorderPanel.Position.East
   }
 
   private class Node_Renderer extends ListView.Renderer[Document.Node.Name] {
@@ -209,7 +229,8 @@
     ): Component = {
       val component = Node_Renderer_Component
       component.node_name = name
-      component.checkbox.selected = nodes_required.contains(name)
+      component.theory_required.selected = theory_required.contains(name)
+      component.document_required.selected = document_required.contains(name)
       component.label_border(name)
       component.label.text = name.theory_base_name
       component
@@ -251,7 +272,8 @@
         GUI_Thread.later {
           continuous_checking.load()
           logic.load ()
-          nodes_required = Document_Model.required_nodes()
+          theory_required = Document_Model.required_nodes(false)
+          document_required = Document_Model.required_nodes(true)
           status.repaint()
         }