--- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Fri Dec 23 22:51:47 2022 +0100
+++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Sat Dec 24 13:19:39 2022 +0100
@@ -175,7 +175,7 @@
class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup") {
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = {
val opt_snapshot =
- Document_Model.get(buffer) match {
+ Document_Model.get_model(buffer) match {
case Some(model) if model.is_theory => Some(Document_Model.snapshot(model))
case _ => None
}
--- a/src/Tools/jEdit/src/document_model.scala Fri Dec 23 22:51:47 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sat Dec 24 13:19:39 2022 +0100
@@ -85,16 +85,17 @@
def document_blobs(): Document.Blobs = state.value.document_blobs
def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
- def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
- def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
+ def get_model(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
+ def get_model(buffer: JEditBuffer): Option[Buffer_Model] =
+ state.value.buffer_models.get(buffer)
def snapshot(model: Document_Model): Document.Snapshot =
PIDE.session.snapshot(
node_name = model.node_name,
pending_edits = Document.Pending_Edits.make(get_models().values))
- def get_snapshot(name: Document.Node.Name): Option[Document.Snapshot] = get(name).map(snapshot)
- def get_snapshot(buffer: JEditBuffer): Option[Document.Snapshot] = get(buffer).map(snapshot)
+ def get_snapshot(name: Document.Node.Name): Option[Document.Snapshot] = get_model(name).map(snapshot)
+ def get_snapshot(buffer: JEditBuffer): Option[Document.Snapshot] = get_model(buffer).map(snapshot)
/* bibtex */
@@ -226,7 +227,7 @@
toggle: Boolean = false,
set: Boolean = false
): Unit =
- Document_Model.get(view.getBuffer).foreach(model =>
+ Document_Model.get_model(view.getBuffer).foreach(model =>
node_required(model.node_name, toggle = toggle, set = set))
@@ -298,7 +299,7 @@
/* HTTP preview */
def open_preview(view: View, plain_text: Boolean): Unit = {
- Document_Model.get(view.getBuffer) match {
+ Document_Model.get_model(view.getBuffer) match {
case Some(model) =>
val url = Preview_Service.server_url(plain_text, model.node_name)
PIDE.editor.hyperlink_url(url).follow(view)
@@ -319,7 +320,7 @@
for {
query <- request.decode_query
name = Library.perhaps_unprefix(plain_text_prefix, query)
- model <- get(PIDE.resources.node_name(name))
+ model <- get_model(PIDE.resources.node_name(name))
}
yield {
val snapshot = model.await_stable_snapshot()
--- a/src/Tools/jEdit/src/isabelle.scala Fri Dec 23 22:51:47 2022 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Sat Dec 24 13:19:39 2022 +0100
@@ -60,7 +60,7 @@
def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
if (buffer == null) None
else
- (JEdit_Lib.buffer_mode(buffer), Document_Model.get(buffer)) match {
+ (JEdit_Lib.buffer_mode(buffer), Document_Model.get_model(buffer)) match {
case ("isabelle", Some(model)) =>
Some(PIDE.session.recent_syntax(model.node_name))
case (mode, _) => mode_syntax(mode)
@@ -328,7 +328,7 @@
): Unit = {
val buffer = text_area.getBuffer
if (!snapshot.is_outdated && text != "") {
- (snapshot.find_command(id), Document_Model.get(buffer)) match {
+ (snapshot.find_command(id), Document_Model.get_model(buffer)) match {
case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
node.command_start(command) match {
case Some(start) =>
--- a/src/Tools/jEdit/src/jedit_editor.scala Fri Dec 23 22:51:47 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sat Dec 24 13:19:39 2022 +0100
@@ -67,7 +67,7 @@
/* current situation */
override def current_node(view: View): Option[Document.Node.Name] =
- GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) }
+ GUI_Thread.require { Document_Model.get_model(view.getBuffer).map(_.node_name) }
override def current_node_snapshot(view: View): Option[Document.Snapshot] =
GUI_Thread.require { Document_Model.get_snapshot(view.getBuffer) }
@@ -85,7 +85,7 @@
case Some(doc_view) if doc_view.model.is_theory =>
snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition)
case _ =>
- Document_Model.get(buffer) match {
+ Document_Model.get_model(buffer) match {
case Some(model) if !model.is_theory =>
snapshot.version.nodes.commands_loading(model.node_name).headOption
case _ => None
--- a/src/Tools/jEdit/src/jedit_resources.scala Fri Dec 23 22:51:47 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Sat Dec 24 13:19:39 2022 +0100
@@ -86,7 +86,7 @@
}
def get_file_content(node_name: Document.Node.Name): Option[String] =
- Document_Model.get(node_name) match {
+ Document_Model.get_model(node_name) match {
case Some(model: Buffer_Model) => Some(JEdit_Lib.buffer_text(model.buffer))
case Some(model: File_Model) => Some(model.content.text)
case None => read_file_content(node_name)
@@ -94,7 +94,7 @@
override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = {
GUI_Thread.now {
- Document_Model.get(name) match {
+ Document_Model.get_model(name) match {
case Some(model: Buffer_Model) =>
JEdit_Lib.buffer_lock(model.buffer) { Some(f(JEdit_Lib.buffer_reader(model.buffer))) }
case Some(model: File_Model) => Some(f(Scan.char_reader(model.content.text)))
--- a/src/Tools/jEdit/src/main_plugin.scala Fri Dec 23 22:51:47 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Sat Dec 24 13:19:39 2022 +0100
@@ -235,7 +235,7 @@
def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
GUI_Thread.now {
JEdit_Lib.buffer_lock(buffer) {
- Document_Model.get(buffer) match {
+ Document_Model.get_model(buffer) match {
case Some(model) => Document_View.init(model, text_area)
case None =>
}