# HG changeset patch
# User wenzelm
# Date 1671884379 -3600
# Node ID 40c8275f01316b4d55bc8b1602d4c21be9949e3c
# Parent  540cd80c5af2c07f2a6066d02777d0646056d536
tuned signature: follow terminology of VSCode_Resources;

diff -r 540cd80c5af2 -r 40c8275f0131 src/Tools/jEdit/jedit_main/isabelle_sidekick.scala
--- 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
       }
diff -r 540cd80c5af2 -r 40c8275f0131 src/Tools/jEdit/src/document_model.scala
--- 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()
diff -r 540cd80c5af2 -r 40c8275f0131 src/Tools/jEdit/src/isabelle.scala
--- 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) =>
diff -r 540cd80c5af2 -r 40c8275f0131 src/Tools/jEdit/src/jedit_editor.scala
--- 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
diff -r 540cd80c5af2 -r 40c8275f0131 src/Tools/jEdit/src/jedit_resources.scala
--- 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)))
diff -r 540cd80c5af2 -r 40c8275f0131 src/Tools/jEdit/src/main_plugin.scala
--- 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 =>
         }