--- a/src/Pure/GUI/gui_thread.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/GUI/gui_thread.scala Tue Dec 20 19:43:55 2022 +0100
@@ -13,13 +13,15 @@
object GUI_Thread {
/* context check */
+ def check(): Boolean = SwingUtilities.isEventDispatchThread()
+
def assert[A](body: => A): A = {
- Predef.assert(SwingUtilities.isEventDispatchThread)
+ Predef.assert(check())
body
}
def require[A](body: => A): A = {
- Predef.require(SwingUtilities.isEventDispatchThread, "GUI thread expected")
+ Predef.require(check(), "GUI thread expected")
body
}
@@ -27,7 +29,7 @@
/* event dispatch queue */
def now[A](body: => A): A = {
- if (SwingUtilities.isEventDispatchThread) body
+ if (check()) body
else {
lazy val result = assert { Exn.capture(body) }
SwingUtilities.invokeAndWait(() => result)
@@ -36,12 +38,12 @@
}
def later(body: => Unit): Unit = {
- if (SwingUtilities.isEventDispatchThread) body
+ if (check()) body
else SwingUtilities.invokeLater(() => body)
}
def future[A](body: => A): Future[A] = {
- if (SwingUtilities.isEventDispatchThread) Future.value(body)
+ if (check()) Future.value(body)
else {
val promise = Future.promise[A]
later { promise.fulfill_result(Exn.capture(body)) }
--- a/src/Pure/PIDE/document.ML Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/PIDE/document.ML Tue Dec 20 19:43:55 2022 +0100
@@ -85,12 +85,13 @@
val no_header: node_header =
{master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
-val no_perspective = make_perspective (false, [], []);
+
+val empty_perspective = make_perspective (false, [], []);
val empty_node =
- make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ());
+ make_node (no_header, NONE, empty_perspective, Entries.empty, NONE, Lazy.value ());
-fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
+fun is_empty_perspective ({required, visible, visible_last, overlays}: perspective) =
not required andalso
Inttab.is_empty visible andalso
is_none visible_last andalso
@@ -99,7 +100,7 @@
fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) =
header = no_header andalso
is_none keywords andalso
- is_no_perspective perspective andalso
+ is_empty_perspective perspective andalso
Entries.is_empty entries andalso
is_none result andalso
Lazy.is_finished consolidated;
--- a/src/Pure/PIDE/document.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/PIDE/document.scala Tue Dec 20 19:43:55 2022 +0100
@@ -181,24 +181,23 @@
/* perspective */
- type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
- type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
-
- val no_perspective_text: Perspective_Text =
- Perspective(false, Text.Perspective.empty, Overlays.empty)
-
- val no_perspective_command: Perspective_Command =
- Perspective(false, Command.Perspective.empty, Overlays.empty)
+ object Perspective_Text {
+ type T = Perspective[Text.Edit, Text.Perspective]
+ val empty: T = Perspective(false, Text.Perspective.empty, Overlays.empty)
+ def is_empty(perspective: T): Boolean =
+ !perspective.required &&
+ perspective.visible.is_empty &&
+ perspective.overlays.is_empty
+ }
- def is_no_perspective_text(perspective: Perspective_Text): Boolean =
- !perspective.required &&
- perspective.visible.is_empty &&
- perspective.overlays.is_empty
-
- def is_no_perspective_command(perspective: Perspective_Command): Boolean =
- !perspective.required &&
- perspective.visible.is_empty &&
- perspective.overlays.is_empty
+ object Perspective_Command {
+ type T = Perspective[Command.Edit, Command.Perspective]
+ val empty: T = Perspective(false, Command.Perspective.empty, Overlays.empty)
+ def is_empty(perspective: T): Boolean =
+ !perspective.required &&
+ perspective.visible.is_empty &&
+ perspective.overlays.is_empty
+ }
/* commands */
@@ -272,14 +271,14 @@
val header: Node.Header = Node.no_header,
val syntax: Option[Outer_Syntax] = None,
val text_perspective: Text.Perspective = Text.Perspective.empty,
- val perspective: Node.Perspective_Command = Node.no_perspective_command,
+ val perspective: Node.Perspective_Command.T = Node.Perspective_Command.empty,
_commands: Node.Commands = Node.Commands.empty
) {
def is_empty: Boolean =
get_blob.isEmpty &&
header == Node.no_header &&
text_perspective.is_empty &&
- Node.is_no_perspective_command(perspective) &&
+ Node.Perspective_Command.is_empty(perspective) &&
commands.isEmpty
def has_header: Boolean = header != Node.no_header
@@ -304,7 +303,7 @@
def update_perspective(
new_text_perspective: Text.Perspective,
- new_perspective: Node.Perspective_Command): Node =
+ new_perspective: Node.Perspective_Command.T): Node =
new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands)
def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] =
@@ -312,7 +311,7 @@
def same_perspective(
other_text_perspective: Text.Perspective,
- other_perspective: Node.Perspective_Command): Boolean =
+ other_perspective: Node.Perspective_Command.T): Boolean =
text_perspective == other_text_perspective &&
perspective.required == other_perspective.required &&
perspective.visible.same(other_perspective.visible) &&
@@ -761,8 +760,7 @@
def get_text(range: Text.Range): Option[String]
- def get_required(document: Boolean): Boolean
- def node_required: Boolean = get_required(false) || get_required(true)
+ def node_required: Boolean
def get_blob: Option[Blob]
def bibtex_entries: List[Text.Info[String]]
@@ -770,7 +768,7 @@
def node_edits(
node_header: Node.Header,
text_edits: List[Text.Edit],
- perspective: Node.Perspective_Text
+ perspective: Node.Perspective_Text.T
): List[Edit_Text] = {
val edits: List[Node.Edit[Text.Edit, Text.Perspective]] =
get_blob match {
--- a/src/Pure/PIDE/document_editor.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala Tue Dec 20 19:43:55 2022 +0100
@@ -46,10 +46,39 @@
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 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,
+ 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)
}
--- a/src/Pure/PIDE/document_status.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/PIDE/document_status.scala Tue Dec 20 19:43:55 2022 +0100
@@ -97,10 +97,25 @@
/* node status */
object Node_Status {
+ val empty: Node_Status =
+ Node_Status(
+ is_suppressed = false,
+ unprocessed = 0,
+ running = 0,
+ warned = 0,
+ failed = 0,
+ finished = 0,
+ canceled = false,
+ terminated = false,
+ initialized = false,
+ finalized = false,
+ consolidated = false)
+
def make(
state: Document.State,
version: Document.Version,
- name: Document.Node.Name): Node_Status = {
+ name: Document.Node.Name
+ ): Node_Status = {
val node = version.nodes(name)
var unprocessed = 0
@@ -156,6 +171,8 @@
finalized: Boolean,
consolidated: Boolean
) {
+ def is_empty: Boolean = this == Node_Status.empty
+
def ok: Boolean = failed == 0
def total: Int = unprocessed + running + warned + failed + finished
@@ -229,11 +246,12 @@
def apply(name: Document.Node.Name): Node_Status = rep(name)
def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
- def present: List[(Document.Node.Name, Node_Status)] =
- (for {
- name <- nodes.topological_order.iterator
- node_status <- get(name)
- } yield (name, node_status)).toList
+ def present(
+ domain: Option[List[Document.Node.Name]] = None
+ ): List[(Document.Node.Name, Node_Status)] = {
+ for (name <- domain.getOrElse(nodes.topological_order))
+ yield name -> get(name).getOrElse(Node_Status.empty)
+ }
def quasi_consolidated(name: Document.Node.Name): Boolean =
rep.get(name) match {
--- a/src/Pure/PIDE/editor.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/PIDE/editor.scala Tue Dec 20 19:43:55 2022 +0100
@@ -20,16 +20,38 @@
protected val document_editor: Synchronized[Document_Editor.State] =
Synchronized(Document_Editor.State())
- def document_editor_session: Option[Sessions.Background] =
- document_editor.value.session_background
- def document_editor_active: Boolean =
- document_editor.value.is_active
- def document_editor_setup(background: Option[Sessions.Background]): Unit =
- document_editor.change(_.copy(session_background = background))
- def document_editor_init(id: AnyRef): Unit =
- document_editor.change(_.register_view(id))
- def document_editor_exit(id: AnyRef): Unit =
- document_editor.change(_.unregister_view(id))
+ 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.required != st1.required, st1)
+ }
+ 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_theories(): List[Document.Node.Name] = document_state().active_document_theories
+
+ def document_setup(background: Option[Sessions.Background]): Unit =
+ 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_select_all(set: Boolean = false): Unit =
+ document_state_change(st => st.select(st.active_document_theories, set = set))
+
+ 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 */
--- a/src/Pure/PIDE/headless.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/PIDE/headless.scala Tue Dec 20 19:43:55 2022 +0100
@@ -390,8 +390,9 @@
val theory_progress =
(for {
- (name, node_status) <- st1.nodes_status.present.iterator
- if changed_st.changed_nodes(name) && !st.already_committed.isDefinedAt(name)
+ (name, node_status) <- st1.nodes_status.present().iterator
+ if !node_status.is_empty && changed_st.changed_nodes(name) &&
+ !st.already_committed.isDefinedAt(name)
p1 = node_status.percentage
if p1 > 0 && !st.nodes_status.get(name).map(_.percentage).contains(p1)
} yield Progress.Theory(name.theory, percentage = Some(p1))).toList
@@ -471,7 +472,7 @@
) {
override def toString: String = node_name.toString
- def node_perspective: Document.Node.Perspective_Text =
+ def node_perspective: Document.Node.Perspective_Text.T =
Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
--- a/src/Pure/Thy/document_build.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/Thy/document_build.scala Tue Dec 20 19:43:55 2022 +0100
@@ -115,10 +115,11 @@
options: Options,
session: String,
dirs: List[Path] = Nil,
- progress: Progress = new Progress
+ progress: Progress = new Progress,
+ verbose: Boolean = false
): Sessions.Background = {
Sessions.load_structure(options + "document=pdf", dirs = dirs).
- selection_deps(Sessions.Selection.session(session), progress = progress).
+ selection_deps(Sessions.Selection.session(session), progress = progress, verbose = verbose).
background(session)
}
--- a/src/Pure/Thy/thy_syntax.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Tue Dec 20 19:43:55 2022 +0100
@@ -258,7 +258,7 @@
case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
- val perspective: Document.Node.Perspective_Command =
+ val perspective: Document.Node.Perspective_Command.T =
Document.Node.Perspective(required, visible_overlay, overlays)
if (node.same_perspective(text_perspective, perspective)) node
else {
--- a/src/Pure/Tools/server.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/Tools/server.scala Tue Dec 20 19:43:55 2022 +0100
@@ -269,7 +269,7 @@
override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {
val json =
- for ((name, node_status) <- nodes_status.present)
+ for ((name, node_status) <- nodes_status.present() if !node_status.is_empty)
yield name.json + ("status" -> node_status.json)
context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
}
--- a/src/Tools/VSCode/src/vscode_model.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala Tue Dec 20 19:43:55 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,21 +70,14 @@
content: VSCode_Model.Content,
version: Option[Long] = None,
external_file: Boolean = false,
- theory_required: Boolean = false,
- document_required: Boolean = false,
- last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
+ 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,
published_decorations: List[VSCode_Model.Decoration] = Nil
) extends Document.Model {
model =>
- /* required */
-
- def get_required(document: Boolean): Boolean =
- if (document) document_required else theory_required
-
-
/* content */
def get_text(range: Text.Range): Option[String] = content.doc.get_text(range)
@@ -111,10 +104,12 @@
def node_perspective(
doc_blobs: Document.Blobs,
caret: Option[Line.Position]
- ): (Boolean, Document.Node.Perspective_Text) = {
+ ): (Boolean, Document.Node.Perspective_Text.T) = {
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) {
@@ -142,9 +137,9 @@
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.no_perspective_text)
+ else (false, Document.Node.Perspective_Text.empty)
}
--- a/src/Tools/VSCode/src/vscode_resources.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Dec 20 19:43:55 2022 +0100
@@ -206,7 +206,10 @@
state.change_result { st =>
val stable_tip_version = session.stable_tip_version(st.models)
- val thy_files = resources.resolve_dependencies(st.models, Nil)
+ val thy_files =
+ resources.resolve_dependencies(st.models,
+ editor.document_required().map((_, Position.none)))
+
val aux_files = stable_tip_version.toList.flatMap(undefined_blobs)
val loaded_models =
--- a/src/Tools/jEdit/src/document_dockable.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Tue Dec 20 19:43:55 2022 +0100
@@ -27,10 +27,6 @@
val FINISHED = Value("finished")
}
- sealed case class Result(output: List[XML.Tree] = Nil) {
- def failed: Boolean = output.exists(Protocol.is_error)
- }
-
object State {
def init(): State = State()
}
@@ -44,8 +40,10 @@
def run(progress: Progress, process: Future[Unit]): State =
copy(progress = progress, process = process, status = Status.RUNNING)
- def finish(result: Result): State = State(output = result.output)
- def finish(msg: XML.Tree): State = finish(Result(output = List(msg)))
+ def finish(output: List[XML.Tree]): State =
+ copy(process = Future.value(()), status = Status.FINISHED, output = output)
+
+ def ok: Boolean = !output.exists(Protocol.is_error)
}
}
@@ -121,73 +119,91 @@
/* document build process */
- private def cancel(): Unit =
- current_state.change { st => st.process.cancel(); st }
-
private def init_state(): Unit =
current_state.change { _ => Document_Dockable.State(progress = log_progress()) }
+ private def cancel_process(): Unit =
+ current_state.change { st => st.process.cancel(); st }
+
+ private def await_process(): Unit =
+ current_state.guarded_access(st => if (st.process.is_finished) None else Some((), st))
+
+ private def finish_process(output: List[XML.Tree]): Unit =
+ current_state.change(_.finish(output))
+
+ private def run_process(body: Document_Editor.Log_Progress => Unit): Boolean = {
+ val started =
+ current_state.change_result { st =>
+ if (st.process.is_finished) {
+ val progress = log_progress()
+ val process =
+ Future.thread[Unit](name = "Document_Dockable.process") {
+ await_process()
+ body(progress)
+ }
+ (true, st.run(progress, process))
+ }
+ else (false, st)
+ }
+ show_state()
+ started
+ }
+
private def load_document(session: String): Boolean = {
- current_state.change_result { st =>
- if (st.process.is_finished) {
- val options = PIDE.options.value
- val progress = log_progress()
- val process =
- Future.thread[Unit](name = "Document_Dockable.load_document") {
- try {
- val session_background =
- Document_Build.session_background(
- options, session, dirs = JEdit_Sessions.session_dirs)
- PIDE.editor.document_editor_setup(Some(session_background))
- GUI_Thread.later { show_state(); show_page(theories_page) }
- }
- catch {
- case exn: Throwable if !Exn.is_interrupt(exn) =>
- current_state.change(_.finish(Protocol.error_message(Exn.message(exn))))
- GUI_Thread.later { show_state(); show_page(output_page) }
- }
+ val options = PIDE.options.value
+ run_process { progress =>
+ try {
+ val session_background =
+ Document_Build.session_background(
+ options, session, dirs = JEdit_Sessions.session_dirs)
+ PIDE.editor.document_setup(Some(session_background))
+
+ finish_process(Nil)
+ GUI_Thread.later {
+ val domain = PIDE.editor.document_theories().toSet
+ theories.update(domain = Some(domain), trim = true, force = true)
+ show_state()
+ show_page(theories_page)
+ }
+ }
+ catch {
+ case exn: Throwable if !Exn.is_interrupt(exn) =>
+ finish_process(List(Protocol.error_message(Exn.print(exn))))
+ GUI_Thread.later {
+ show_state()
+ show_page(output_page)
}
- (true, st.run(progress, process))
}
- else (false, st)
}
}
private def build_document(): Unit = {
- current_state.change { st =>
- if (st.process.is_finished) {
- val progress = log_progress()
- val process =
- Future.thread[Unit](name = "Document_Dockable.build_document") {
- show_page(theories_page)
- Time.seconds(2.0).sleep()
+ run_process { progress =>
+ show_page(theories_page)
+ Time.seconds(2.0).sleep()
- show_page(log_page)
- val res =
- Exn.capture {
- progress.echo("Start " + Date.now())
- for (i <- 1 to 200) {
- progress.echo("message " + i)
- Time.seconds(0.1).sleep()
- }
- progress.echo("Stop " + Date.now())
- }
- val msg =
- res match {
- case Exn.Res(_) => Protocol.writeln_message("OK")
- case Exn.Exn(exn) => Protocol.error_message(Exn.message(exn))
- }
- current_state.change(_.finish(msg))
- show_state()
+ show_page(log_page)
+ val res =
+ Exn.capture {
+ progress.echo("Start " + Date.now())
+ for (i <- 1 to 200) {
+ progress.echo("message " + i)
+ Time.seconds(0.1).sleep()
+ }
+ progress.echo("Stop " + Date.now())
+ }
+ val msg =
+ res match {
+ case Exn.Res(_) => Protocol.writeln_message("OK")
+ case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn))
+ }
+ finish_process(List(msg))
- show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
- GUI_Thread.later { progress.load() }
- }
- st.run(progress, process)
- }
- else st
+ show_state()
+
+ show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
+ GUI_Thread.later { progress.load() }
}
- show_state()
}
@@ -214,7 +230,7 @@
private val cancel_button =
new GUI.Button("Cancel") {
tooltip = "Cancel build process"
- override def clicked(): Unit = cancel()
+ override def clicked(): Unit = cancel_process()
}
private val view_button =
@@ -234,10 +250,26 @@
/* message pane with pages */
+ private val select_all_button =
+ new GUI.Button("All") {
+ tooltip = "Select all document theories"
+ override def clicked(): Unit = PIDE.editor.document_select_all(set = true)
+ }
+
+ private val select_none_button =
+ new GUI.Button("None") {
+ tooltip = "Deselect all document theories"
+ override def clicked(): Unit = PIDE.editor.document_select_all(set = false)
+ }
+
+ private val theories_controls =
+ Wrap_Panel(List(select_all_button, select_none_button))
+
private val theories = new Theories_Status(view, document = true)
private val theories_page =
new TabbedPane.Page("Theories", new BorderPanel {
+ layout(theories_controls) = BorderPanel.Position.North
layout(theories.gui) = BorderPanel.Position.Center
}, "Selection and status of document theories")
@@ -268,20 +300,20 @@
GUI_Thread.later {
document_session.load()
handle_resize()
- theories.reinit()
+ theories.refresh()
}
case changed: Session.Commands_Changed =>
GUI_Thread.later {
- theories.update(domain = Some(changed.nodes), trim = changed.assignment)
+ val domain = PIDE.editor.document_theories().filter(changed.nodes).toSet
+ if (domain.nonEmpty) theories.update(domain = Some(domain))
}
}
override def init(): Unit = {
- PIDE.editor.document_editor_init(dockable)
+ PIDE.editor.document_init(dockable)
init_state()
PIDE.session.global_options += main
PIDE.session.commands_changed += main
- theories.update()
handle_resize()
delay_load.invoke()
}
@@ -290,6 +322,6 @@
PIDE.session.global_options -= main
PIDE.session.commands_changed -= main
delay_resize.revoke()
- PIDE.editor.document_editor_exit(dockable)
+ PIDE.editor.document_exit(dockable)
}
}
--- a/src/Tools/jEdit/src/document_model.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Tue Dec 20 19:43:55 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,30 +200,26 @@
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)
}
})
- if (changed) {
- PIDE.plugin.options_changed()
- PIDE.editor.flush()
- }
+ if (changed) PIDE.editor.state_changed()
}
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 */
@@ -340,12 +335,14 @@
def node_perspective(
doc_blobs: Document.Blobs,
hidden: Boolean
- ): (Boolean, Document.Node.Perspective_Text) = {
+ ): (Boolean, Document.Node.Perspective_Text.T) = {
GUI_Thread.require {}
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,9 +353,9 @@
}
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.no_perspective_text)
+ else (false, Document.Node.Perspective_Text.empty)
}
@@ -377,23 +374,21 @@
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.no_perspective_text, 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,
- last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
+ node_required: Boolean = false,
+ last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty,
pending_edits: List[Text.Edit] = Nil
): File_Model = {
val file = JEdit_Lib.check_file(node_name.node)
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,
- last_perspective: Document.Node.Perspective_Text,
+ 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 */
@@ -469,10 +459,10 @@
def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
if (pending_edits.nonEmpty ||
!File_Format.registry.is_theory(node_name) &&
- (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
+ (node_required || !Document.Node.Perspective_Text.is_empty(last_perspective))) None
else {
val text_edits = List(Text.Edit.remove(0, content.text))
- Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text))
+ Some(node_edits(Document.Node.no_header, text_edits, Document.Node.Perspective_Text.empty))
}
@@ -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 {
@@ -586,12 +572,12 @@
private object pending_edits {
private val pending = new mutable.ListBuffer[Text.Edit]
- private var last_perspective = Document.Node.no_perspective_text
+ private var last_perspective = Document.Node.Perspective_Text.empty
def nonEmpty: Boolean = synchronized { pending.nonEmpty }
def get_edits: List[Text.Edit] = synchronized { pending.toList }
- def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
- def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
+ def get_last_perspective: Document.Node.Perspective_Text.T = synchronized { last_perspective }
+ def set_last_perspective(perspective: Document.Node.Perspective_Text.T): Unit =
synchronized { last_perspective = perspective }
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
@@ -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)
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Dec 20 19:43:55 2022 +0100
@@ -53,6 +53,17 @@
} yield doc_view.model.node_name).contains(name)
+ /* global changes */
+
+ def state_changed(): Unit = {
+ GUI_Thread.later { flush() }
+ PIDE.plugin.deps_changed()
+ session.global_options.post(Session.Global_Options(PIDE.options.value))
+ }
+
+ override def document_state_changed(): Unit = state_changed()
+
+
/* current situation */
override def current_node(view: View): Option[Document.Node.Name] =
--- a/src/Tools/jEdit/src/main_plugin.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Tue Dec 20 19:43:55 2022 +0100
@@ -86,23 +86,23 @@
val spell_checker = new Spell_Checker_Variable
- /* global changes */
-
- def options_changed(): Unit = {
- session.global_options.post(Session.Global_Options(options.value))
- delay_load.invoke()
- }
-
- def deps_changed(): Unit = {
- delay_load.invoke()
- }
-
-
/* theory files */
- lazy val delay_init: Delay =
+ private lazy val delay_init: Delay =
Delay.last(PIDE.session.load_delay, gui = true) { init_models() }
+ private lazy val delay_load: Delay =
+ Delay.last(session.load_delay, gui = true) {
+ if (JEdit_Options.continuous_checking()) {
+ if (!PerspectiveManager.isPerspectiveEnabled ||
+ JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
+ else if (delay_load_activated()) delay_load_body()
+ else delay_load.invoke()
+ }
+ }
+
+ def deps_changed(): Unit = delay_load.invoke()
+
private val delay_load_active = Synchronized(false)
private def delay_load_finished(): Unit = delay_load_active.change(_ => false)
private def delay_load_activated(): Boolean =
@@ -112,7 +112,9 @@
val required_files = {
val models = Document_Model.get_models()
- val thy_files = resources.resolve_dependencies(models, Nil)
+ val thy_files =
+ resources.resolve_dependencies(models,
+ PIDE.editor.document_required().map((_, Position.none)))
val aux_files =
if (resources.auto_resolve) {
@@ -148,16 +150,6 @@
else delay_load_finished()
}
- private lazy val delay_load: Delay =
- Delay.last(session.load_delay, gui = true) {
- if (JEdit_Options.continuous_checking()) {
- if (!PerspectiveManager.isPerspectiveEnabled ||
- JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
- else if (delay_load_activated()) delay_load_body()
- else delay_load.invoke()
- }
- }
-
private def file_watcher_action(changed: Set[JFile]): Unit =
if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Dec 20 19:43:55 2022 +0100
@@ -48,8 +48,8 @@
/* main */
- val status = new Theories_Status(view)
- set_content(new ScrollPane(status.gui))
+ private val theories = new Theories_Status(view)
+ set_content(new ScrollPane(theories.gui))
private val main =
Session.Consumer[Any](getClass.getName) {
@@ -60,11 +60,11 @@
GUI_Thread.later {
continuous_checking.load()
logic.load()
- status.reinit()
+ theories.refresh()
}
case changed: Session.Commands_Changed =>
- GUI_Thread.later { status.update(domain = Some(changed.nodes), trim = changed.assignment) }
+ GUI_Thread.later { theories.update(domain = Some(changed.nodes), trim = changed.assignment) }
}
override def init(): Unit = {
@@ -73,7 +73,7 @@
PIDE.session.commands_changed += main
handle_phase(PIDE.session.phase)
- status.update()
+ theories.update()
}
override def exit(): Unit = {
--- a/src/Tools/jEdit/src/theories_status.scala Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala Tue Dec 20 19:43:55 2022 +0100
@@ -24,8 +24,18 @@
/* component state -- owned by GUI thread */
private var nodes_status = Document_Status.Nodes_Status.empty
- 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 var nodes_required = Set.empty[Document.Node.Name]
+ private var document_required = Set.empty[Document.Node.Name]
+
+ private def init_state(): Unit = GUI_Thread.require {
+ if (document) {
+ nodes_required = PIDE.editor.document_required().toSet
+ }
+ else {
+ nodes_required = Document_Model.nodes_required()
+ document_required = PIDE.editor.document_required().toSet
+ }
+ }
/* node renderer */
@@ -51,6 +61,9 @@
}
private class Node_Renderer extends ListView.Renderer[Document.Node.Name] {
+ private val document_marker = Symbol.decode(" \\<^file>")
+ private val no_document_marker = " "
+
private object component extends BorderPanel {
opaque = true
border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
@@ -143,10 +156,11 @@
index: Int
): Component = {
component.node_name = name
- component.required.selected =
- (if (document) document_required else theory_required).contains(name)
+ component.required.selected = nodes_required.contains(name)
component.label_border(name)
- component.label.text = name.theory_base_name
+ component.label.text =
+ name.theory_base_name +
+ (if (document_required.contains(name)) document_marker else no_document_marker)
component
}
}
@@ -172,7 +186,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)
@@ -203,7 +219,11 @@
/* update */
- def update(domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false): Unit = {
+ def update(
+ domain: Option[Set[Document.Node.Name]] = None,
+ trim: Boolean = false,
+ force: Boolean = false
+ ): Unit = {
GUI_Thread.require {}
val snapshot = PIDE.session.snapshot()
@@ -213,23 +233,27 @@
PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
nodes_status = nodes_status1
- if (nodes_status_changed) {
+ if (nodes_status_changed || force) {
gui.listData =
- (for {
- (name, node_status) <- nodes_status1.present.iterator
- if !node_status.is_suppressed && node_status.total > 0
- } yield name).toList
+ if (document) {
+ nodes_status1.present(domain = Some(PIDE.editor.document_theories())).map(_._1)
+ }
+ else {
+ (for {
+ (name, node_status) <- nodes_status1.present().iterator
+ if !node_status.is_empty && !node_status.is_suppressed && node_status.total > 0
+ } yield name).toList
+ }
}
}
- /* reinit */
+ /* refresh */
- def reinit(): Unit = {
- GUI_Thread.require {}
-
- theory_required = Document_Model.required_nodes(false)
- document_required = Document_Model.required_nodes(true)
+ def refresh(): Unit = GUI_Thread.require {
+ init_state()
gui.repaint()
}
+
+ init_state()
}