--- a/src/Pure/PIDE/document.scala Tue Nov 08 08:41:29 2022 +0100
+++ b/src/Pure/PIDE/document.scala Tue Nov 08 08:41:48 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]]
--- a/src/Tools/VSCode/src/vscode_model.scala Tue Nov 08 08:41:29 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala Tue Nov 08 08:41:48 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 */
--- a/src/Tools/jEdit/src/document_model.scala Tue Nov 08 08:41:29 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Tue Nov 08 08:41:48 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)
}
}
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue Nov 08 08:41:29 2022 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Nov 08 08:41:48 2022 +0100
@@ -10,7 +10,7 @@
import isabelle._
import scala.swing.{Button, TextArea, Label, ListView, Alignment,
- ScrollPane, Component, CheckBox, BorderPanel}
+ ScrollPane, Component, CheckBox, BorderPanel, BoxPanel, Orientation}
import scala.swing.event.{MouseClicked, MouseMoved}
import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
@@ -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,7 +214,11 @@
BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2))
}
- layout(checkbox) = BorderPanel.Position.West
+ val required = new BoxPanel(Orientation.Horizontal)
+ required.contents += theory_required
+ // FIXME required.contents += document_required
+
+ layout(required) = BorderPanel.Position.West
layout(label) = BorderPanel.Position.Center
}
@@ -209,7 +232,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 +275,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()
}