--- a/src/Pure/PIDE/document.scala Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Pure/PIDE/document.scala Mon Dec 26 19:13:37 2022 +0100
@@ -796,7 +796,7 @@
def node_required: Boolean
def get_blob: Option[Blob]
- def bibtex_entries: List[Text.Info[String]]
+ def bibtex_entries: Bibtex.Entries
def node_edits(
node_header: Node.Header,
--- a/src/Pure/Thy/bibtex.scala Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Pure/Thy/bibtex.scala Mon Dec 26 19:13:37 2022 +0100
@@ -154,35 +154,61 @@
/* entries */
- def entries(text: String): List[Text.Info[String]] = {
- val result = new mutable.ListBuffer[Text.Info[String]]
- var offset = 0
- for (chunk <- Bibtex.parse(text)) {
- val end_offset = offset + chunk.source.length
- if (chunk.name != "" && !chunk.is_command)
- result += Text.Info(Text.Range(offset, end_offset), chunk.name)
- offset = end_offset
+ object Entries {
+ val empty: Entries = apply(Nil)
+
+ def apply(entries: List[Text.Info[String]], errors: List[String] = Nil): Entries =
+ new Entries(entries, errors)
+
+ def parse(text: String, file_pos: String = ""): Entries = {
+ val entries = new mutable.ListBuffer[Text.Info[String]]
+ var offset = 0
+ var line = 1
+ var err_line = 0
+
+ try {
+ for (chunk <- Bibtex.parse(text)) {
+ val end_offset = offset + chunk.source.length
+ if (chunk.name != "" && !chunk.is_command) {
+ entries += Text.Info(Text.Range(offset, end_offset), chunk.name)
+ }
+ if (chunk.is_malformed && err_line == 0) { err_line = line }
+ offset = end_offset
+ line += chunk.source.count(_ == '\n')
+ }
+
+ val err_pos =
+ if (err_line == 0 || file_pos.isEmpty) Position.none
+ else Position.Line_File(err_line, file_pos)
+ val errors =
+ if (err_line == 0) Nil
+ else List("Malformed bibtex file" + Position.here(err_pos))
+
+ apply(entries.toList, errors = errors)
+ }
+ catch { case ERROR(msg) => apply(Nil, errors = List(msg)) }
}
- result.toList
+
+ def iterator[A <: Document.Model](models: Iterable[A]): Iterator[Text.Info[(String, A)]] =
+ for {
+ model <- models.iterator
+ info <- model.bibtex_entries.entries.iterator
+ } yield info.map((_, model))
}
- def entries_iterator[A, B <: Document.Model](
- models: Map[A, B]
- ): Iterator[Text.Info[(String, B)]] = {
- for {
- (_, model) <- models.iterator
- info <- model.bibtex_entries.iterator
- } yield info.map((_, model))
+ final class Entries private(val entries: List[Text.Info[String]], val errors: List[String]) {
+ def ::: (other: Entries): Entries =
+ new Entries(entries ::: other.entries, errors ::: other.errors)
}
/* completion */
- def completion[A, B <: Document.Model](
+ def completion[A <: Document.Model](
history: Completion.History,
rendering: Rendering,
caret: Text.Offset,
- models: Map[A, B]
+ models: Iterable[A]
): Option[Completion.Result] = {
for {
Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption
@@ -193,7 +219,7 @@
entries =
(for {
- Text.Info(_, (entry, _)) <- entries_iterator(models)
+ Text.Info(_, (entry, _)) <- Entries.iterator(models)
if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1
} yield entry).toList
if entries.nonEmpty
@@ -382,7 +408,7 @@
}
def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
- def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)
+ def is_malformed: Boolean = tokens.exists(_.is_malformed)
def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined
}
--- a/src/Pure/Thy/sessions.scala Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Dec 26 19:13:37 2022 +0100
@@ -439,9 +439,7 @@
try { Path.check_case_insensitive(session_files ::: imported_files); Nil }
catch { case ERROR(msg) => List(msg) }
- val bibtex_errors =
- try { info.bibtex_entries; Nil }
- catch { case ERROR(msg) => List(msg) }
+ val bibtex_errors = info.bibtex_entries.errors
val base =
Base(
@@ -639,12 +637,14 @@
def browser_info: Boolean = options.bool("browser_info")
- lazy val bibtex_entries: List[Text.Info[String]] =
+ lazy val bibtex_entries: Bibtex.Entries =
(for {
(document_dir, file) <- document_files.iterator
if File.is_bib(file.file_name)
- info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator
- } yield info).toList
+ } yield {
+ val path = dir + document_dir + file
+ Bibtex.Entries.parse(File.read(path), file_pos = path.expand.implode)
+ }).foldRight(Bibtex.Entries.empty)(_ ::: _)
def record_proofs: Boolean = options.int("record_proofs") >= 2
@@ -923,11 +923,12 @@
def imports_topological_order: List[String] = imports_graph.topological_order
def bibtex_entries: List[(String, List[String])] =
- build_topological_order.flatMap(name =>
- apply(name).bibtex_entries match {
+ build_topological_order.flatMap { name =>
+ apply(name).bibtex_entries.entries match {
case Nil => None
case entries => Some(name -> entries.map(_.info))
- })
+ }
+ }
override def toString: String =
imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
--- a/src/Tools/VSCode/src/vscode_model.scala Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala Mon Dec 26 19:13:37 2022 +0100
@@ -26,11 +26,7 @@
/* content */
- object Content {
- val empty: Content = Content(Line.Document.empty)
- }
-
- sealed case class Content(doc: Line.Document) {
+ sealed case class Content(node_name: Document.Node.Name, doc: Line.Document) {
override def toString: String = doc.toString
def text_length: Text.Offset = doc.text_length
def text_range: Text.Range = doc.text_range
@@ -38,9 +34,7 @@
lazy val bytes: Bytes = Bytes(Symbol.encode(text))
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
- lazy val bibtex_entries: List[Text.Info[String]] =
- try { Bibtex.entries(text) }
- catch { case ERROR(_) => Nil }
+ lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text, file_pos = node_name.node)
def recode_symbols: List[LSP.TextEdit] =
(for {
@@ -58,15 +52,15 @@
editor: Language_Server.Editor,
node_name: Document.Node.Name
): VSCode_Model = {
- VSCode_Model(session, editor, node_name, Content.empty,
- node_required = File_Format.registry.is_theory(node_name))
+ val content = Content(node_name, Line.Document.empty)
+ val is_theory = File_Format.registry.is_theory(node_name)
+ VSCode_Model(session, editor, content, node_required = is_theory)
}
}
sealed case class VSCode_Model(
session: Session,
editor: Language_Server.Editor,
- node_name: Document.Node.Name,
content: VSCode_Model.Content,
version: Option[Long] = None,
external_file: Boolean = false,
@@ -81,6 +75,8 @@
/* content */
+ def node_name: Document.Node.Name = content.node_name
+
def get_text(range: Text.Range): Option[String] = content.doc.get_text(range)
def set_version(new_version: Long): VSCode_Model = copy(version = Some(new_version))
@@ -153,8 +149,7 @@
/* bibtex entries */
- def bibtex_entries: List[Text.Info[String]] =
- model.content.bibtex_entries
+ def bibtex_entries: Bibtex.Entries = model.content.bibtex_entries
/* edits */
@@ -166,7 +161,7 @@
Text.Edit.replace(0, content.text, insert) match {
case Nil => None
case edits =>
- val content1 = VSCode_Model.Content(Line.Document(insert))
+ val content1 = VSCode_Model.Content(node_name, Line.Document(insert))
Some(copy(content = content1, pending_edits = pending_edits ::: edits))
}
case Some(remove) =>
@@ -174,7 +169,7 @@
case None => error("Failed to apply document change: " + remove)
case Some((Nil, _)) => None
case Some((edits, doc1)) =>
- val content1 = VSCode_Model.Content(doc1)
+ val content1 = VSCode_Model.Content(node_name, doc1)
Some(copy(content = content1, pending_edits = pending_edits ::: edits))
}
}
--- a/src/Tools/VSCode/src/vscode_rendering.scala Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Mon Dec 26 19:13:37 2022 +0100
@@ -78,7 +78,7 @@
/* bibtex */
def bibtex_entries_iterator(): Iterator[Text.Info[(String, VSCode_Model)]] =
- Bibtex.entries_iterator(resources.get_models())
+ Bibtex.Entries.iterator(resources.get_models())
def bibtex_completion(history: Completion.History, caret: Text.Offset): Option[Completion.Result] =
Bibtex.completion(history, rendering, caret, resources.get_models())
--- a/src/Tools/VSCode/src/vscode_resources.scala Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Dec 26 19:13:37 2022 +0100
@@ -113,8 +113,8 @@
else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path)))
}
- def get_models(): Map[JFile, VSCode_Model] = state.value.models
- def get_model(file: JFile): Option[VSCode_Model] = get_models().get(file)
+ def get_models(): Iterable[VSCode_Model] = state.value.models.values
+ def get_model(file: JFile): Option[VSCode_Model] = state.value.models.get(file)
def get_model(name: Document.Node.Name): Option[VSCode_Model] = get_model(node_file(name))
@@ -123,7 +123,7 @@
def snapshot(model: VSCode_Model): Document.Snapshot =
model.session.snapshot(
node_name = model.node_name,
- pending_edits = Document.Pending_Edits.make(get_models().values))
+ pending_edits = Document.Pending_Edits.make(get_models()))
def get_snapshot(file: JFile): Option[Document.Snapshot] =
get_model(file).map(snapshot)
--- a/src/Tools/jEdit/src/document_model.scala Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Mon Dec 26 19:13:37 2022 +0100
@@ -73,7 +73,8 @@
if (models.isDefinedAt(node_name)) this
else {
val edit = Text.Edit.insert(0, text)
- val model = File_Model.init(session, node_name, text, pending_edits = List(edit))
+ val content = File_Content(node_name, text)
+ val model = File_Model.init(session, content = content, pending_edits = List(edit))
copy(models = models + (node_name -> model))
}
}
@@ -84,15 +85,16 @@
def document_blobs(): Document.Blobs = state.value.document_blobs
- def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
- def get_model(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
+ def get_models_map(): Map[Document.Node.Name, Document_Model] = state.value.models
+ def get_models(): Iterable[Document_Model] = get_models_map().values
+ def get_model(name: Document.Node.Name): Option[Document_Model] = get_models_map().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))
+ pending_edits = Document.Pending_Edits.make(get_models()))
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)
@@ -101,11 +103,11 @@
/* bibtex */
def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
- Bibtex.entries_iterator(state.value.models)
+ Bibtex.Entries.iterator(get_models())
def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
: Option[Completion.Result] =
- Bibtex.completion(history, rendering, caret, state.value.models)
+ Bibtex.completion(history, rendering, caret, get_models())
/* overlays */
@@ -131,7 +133,7 @@
text <- PIDE.resources.read_file_content(node_name)
if model.content.text != text
} yield {
- val content = Document_Model.File_Content(text)
+ val content = Document_Model.File_Content(node_name, text)
val edits = Text.Edit.replace(0, model.content.text, text)
(node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
}).toList
@@ -287,12 +289,18 @@
/* file content */
- sealed case class File_Content(text: String) {
+ object File_Content {
+ val empty: File_Content = apply(Document.Node.Name.empty, "")
+
+ def apply(node_name: Document.Node.Name, text: String): File_Content =
+ new File_Content(node_name, text)
+ }
+
+ final class File_Content private(val node_name: Document.Node.Name, val text: String) {
+ override def toString: String = "Document_Model.File_Content(" + node_name.node + ")"
lazy val bytes: Bytes = Bytes(Symbol.encode(text))
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
- lazy val bibtex_entries: List[Text.Info[String]] =
- try { Bibtex.entries(text) }
- catch { case ERROR(_) => Nil }
+ lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text, file_pos = node_name.node)
}
@@ -384,46 +392,43 @@
}
object File_Model {
- def empty(session: Session): File_Model =
- File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
- false, Document.Node.Perspective_Text.empty, Nil)
-
def init(session: Session,
- node_name: Document.Node.Name,
- text: String,
+ content: Document_Model.File_Content = Document_Model.File_Content.empty,
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 node_name = content.node_name
+
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 node_required1 = node_required || File_Format.registry.is_theory(node_name)
- File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
+ File_Model(session, file, content, node_required1, last_perspective, pending_edits)
}
}
case class File_Model(
session: Session,
- node_name: Document.Node.Name,
file: Option[JFile],
content: Document_Model.File_Content,
node_required: Boolean,
last_perspective: Document.Node.Perspective_Text.T,
pending_edits: List[Text.Edit]
) extends Document_Model {
+ /* content */
+
+ def node_name: Document.Node.Name = content.node_name
+
+ def get_text(range: Text.Range): Option[String] =
+ range.try_substring(content.text)
+
+
/* required */
def set_node_required(b: Boolean): File_Model = copy(node_required = b)
- /* text */
-
- def get_text(range: Text.Range): Option[String] =
- range.try_substring(content.text)
-
-
/* header */
def node_header: Document.Node.Header =
@@ -441,8 +446,8 @@
if (is_theory) None
else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
- def bibtex_entries: List[Text.Info[String]] =
- if (File.is_bib(node_name.node)) content.bibtex_entries else Nil
+ def bibtex_entries: Bibtex.Entries =
+ if (File.is_bib(node_name.node)) content.bibtex_entries else Bibtex.Entries.empty
/* edits */
@@ -451,7 +456,7 @@
Text.Edit.replace(0, content.text, text) match {
case Nil => None
case edits =>
- val content1 = Document_Model.File_Content(text)
+ val content1 = Document_Model.File_Content(node_name, text)
val pending_edits1 = pending_edits ::: edits
Some(copy(content = content1, pending_edits = pending_edits1))
}
@@ -502,11 +507,6 @@
/* 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 }
-
def document_view_iterator: Iterator[Document_View] =
for {
text_area <- JEdit_Lib.jedit_text_areas(buffer)
@@ -523,88 +523,38 @@
}
- /* blob */
-
- // owned by GUI thread
- private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None
-
- private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
+ /* mutable buffer state: owned by GUI thread */
- def get_blob: Option[Document.Blob] =
- GUI_Thread.require {
- if (is_theory) None
- else {
- val (bytes, text, chunk) =
- _blob match {
- case Some(x) => x
- case None =>
- val bytes = PIDE.resources.make_file_content(buffer)
- val text = buffer.getText(0, buffer.getLength)
- val chunk = Symbol.Text_Chunk(text)
- val x = (bytes, text, chunk)
- _blob = Some(x)
- x
- }
- val changed = !buffer_edits.is_empty
- Some(Document.Blob(bytes, text, chunk, changed))
- }
- }
-
-
- /* bibtex entries */
+ private object buffer_state {
+ // perspective and edits
- // owned by GUI thread
- private var _bibtex_entries: Option[List[Text.Info[String]]] = None
-
- private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
+ private var last_perspective = Document.Node.Perspective_Text.empty
+ def get_last_perspective: Document.Node.Perspective_Text.T =
+ GUI_Thread.require { last_perspective }
+ def set_last_perspective(perspective: Document.Node.Perspective_Text.T): Unit =
+ GUI_Thread.require { last_perspective = perspective }
- def bibtex_entries: List[Text.Info[String]] =
- GUI_Thread.require {
- if (File.is_bib(node_name.node)) {
- _bibtex_entries match {
- case Some(entries) => entries
- case None =>
- val text = JEdit_Lib.buffer_text(buffer)
- val entries =
- try { Bibtex.entries(text) }
- catch { case ERROR(msg) => Output.warning(msg); Nil }
- _bibtex_entries = Some(entries)
- entries
- }
- }
- else Nil
- }
+ private var node_required = false
+ def get_node_required: Boolean = GUI_Thread.require { node_required }
+ def set_node_required(b: Boolean): Unit = GUI_Thread.require { node_required = b }
-
- /* pending buffer edits */
-
- private object buffer_edits {
- private val pending = new mutable.ListBuffer[Text.Edit]
- private var last_perspective = Document.Node.Perspective_Text.empty
-
- def is_empty: Boolean = synchronized { pending.isEmpty }
- def get_edits: List[Text.Edit] = synchronized { pending.toList }
- 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 }
+ private val pending_edits = new mutable.ListBuffer[Text.Edit]
+ def is_stable: Boolean = GUI_Thread.require { pending_edits.isEmpty }
+ def get_pending_edits: List[Text.Edit] = GUI_Thread.require { pending_edits.toList }
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
- synchronized {
- GUI_Thread.require {}
-
- val edits = get_edits
+ GUI_Thread.require {
+ val edits = get_pending_edits
val (reparse, perspective) = node_perspective(doc_blobs, hidden)
if (reparse || edits.nonEmpty || last_perspective != perspective) {
- pending.clear()
+ pending_edits.clear()
last_perspective = perspective
node_edits(node_header(), edits, perspective)
}
else Nil
}
- def edit(edits: List[Text.Edit]): Unit = synchronized {
- GUI_Thread.require {}
-
+ def edit(edits: List[Text.Edit]): Unit = GUI_Thread.require {
reset_blob()
reset_bibtex_entries()
@@ -612,16 +562,66 @@
doc_view.rich_text_area.active_reset()
}
- pending ++= edits
+ pending_edits ++= edits
PIDE.editor.invoke()
}
+
+
+ // blob
+
+ private var blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None
+
+ def reset_blob(): Unit = GUI_Thread.require { blob = None }
+
+ def get_blob: Option[Document.Blob] = GUI_Thread.require {
+ if (is_theory) None
+ else {
+ val (bytes, text, chunk) =
+ blob getOrElse {
+ val bytes = PIDE.resources.make_file_content(buffer)
+ val text = buffer.getText(0, buffer.getLength)
+ val chunk = Symbol.Text_Chunk(text)
+ val x = (bytes, text, chunk)
+ blob = Some(x)
+ x
+ }
+ val changed = !is_stable
+ Some(Document.Blob(bytes, text, chunk, changed))
+ }
+ }
+
+
+ // bibtex entries
+
+ private var bibtex_entries: Option[Bibtex.Entries] = None
+
+ def reset_bibtex_entries(): Unit = GUI_Thread.require { bibtex_entries = None }
+
+ def get_bibtex_entries: Bibtex.Entries = GUI_Thread.require {
+ if (File.is_bib(node_name.node)) {
+ bibtex_entries getOrElse {
+ val text = JEdit_Lib.buffer_text(buffer)
+ val entries = Bibtex.Entries.parse(text, file_pos = node_name.node)
+ if (entries.errors.nonEmpty) Output.warning(cat_lines(entries.errors))
+ bibtex_entries = Some(entries)
+ entries
+ }
+ }
+ else Bibtex.Entries.empty
+ }
}
- def is_stable: Boolean = buffer_edits.is_empty
- def pending_edits: List[Text.Edit] = buffer_edits.get_edits
+ def is_stable: Boolean = buffer_state.is_stable
+ def pending_edits: List[Text.Edit] = buffer_state.get_pending_edits
+ def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
+ buffer_state.flush_edits(doc_blobs, hidden)
- def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
- buffer_edits.flush_edits(doc_blobs, hidden)
+ def node_required: Boolean = buffer_state.get_node_required
+ def set_node_required(b: Boolean): Unit = buffer_state.set_node_required(b)
+
+ def get_blob: Option[Document.Blob] = buffer_state.get_blob
+
+ def bibtex_entries: Bibtex.Entries = buffer_state.get_bibtex_entries
/* buffer listener */
@@ -634,7 +634,7 @@
num_lines: Int,
length: Int
): Unit = {
- buffer_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
+ buffer_state.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
}
override def preContentRemoved(
@@ -644,7 +644,7 @@
num_lines: Int,
removed_length: Int
): Unit = {
- buffer_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
+ buffer_state.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
}
}
@@ -672,16 +672,14 @@
/* init */
- def init(old_model: Option[File_Model]): Buffer_Model = {
- GUI_Thread.require {}
-
+ def init(old_model: Option[File_Model]): Buffer_Model = GUI_Thread.require {
old_model match {
case None =>
- buffer_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
+ buffer_state.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
case Some(file_model) =>
set_node_required(file_model.node_required)
- buffer_edits.set_last_perspective(file_model.last_perspective)
- buffer_edits.edit(
+ buffer_state.set_last_perspective(file_model.last_perspective)
+ buffer_state.edit(
file_model.pending_edits :::
Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
}
@@ -695,15 +693,14 @@
/* exit */
- def exit(): File_Model = {
- GUI_Thread.require {}
-
+ def exit(): File_Model = GUI_Thread.require {
buffer.removeBufferListener(buffer_listener)
init_token_marker()
- File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer),
- node_required = _node_required,
- last_perspective = buffer_edits.get_last_perspective,
+ File_Model.init(session,
+ content = Document_Model.File_Content(node_name, JEdit_Lib.buffer_text(buffer)),
+ node_required = node_required,
+ last_perspective = buffer_state.get_last_perspective,
pending_edits = pending_edits)
}
}
--- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Dec 26 19:13:37 2022 +0100
@@ -87,7 +87,7 @@
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = {
Pretty_Tooltip.invoke(() =>
{
- val model = File_Model.empty(PIDE.session)
+ val model = File_Model.init(PIDE.session)
val rendering = JEdit_Rendering(snapshot, model, options)
val info = Text.Info(Text.Range.offside, body)
Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
--- a/src/Tools/jEdit/src/jedit_lib.scala Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Dec 26 19:13:37 2022 +0100
@@ -59,10 +59,10 @@
}
- /* files */
+ /* plain files */
def is_file(name: String): Boolean =
- VFSManager.getVFSForPath(name).isInstanceOf[FileVFS]
+ name != null && name.nonEmpty && VFSManager.getVFSForPath(name).isInstanceOf[FileVFS]
def check_file(name: String): Option[JFile] =
if (is_file(name)) Some(new JFile(name)) else None
--- a/src/Tools/jEdit/src/jedit_rendering.scala Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Dec 26 19:13:37 2022 +0100
@@ -32,7 +32,7 @@
): (String, JEdit_Rendering) = {
val command = Command.rich_text(Document_ID.make(), results, formatted_body)
val snippet = snapshot.snippet(command)
- val model = File_Model.empty(PIDE.session)
+ val model = File_Model.init(PIDE.session)
val rendering = apply(snippet, model, PIDE.options.value)
(command.source, rendering)
}
--- a/src/Tools/jEdit/src/jedit_resources.scala Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Dec 26 19:13:37 2022 +0100
@@ -116,7 +116,7 @@
def content(): Bytes = Bytes(this.buf, 0, this.count)
}
- private class File_Content(buffer: Buffer)
+ private class File_Content_Request(buffer: Buffer)
extends BufferIORequest(null, buffer, null, VFSManager.getVFSForPath(buffer.getPath), buffer.getPath) {
def _run(): Unit = {}
def content(): Bytes = {
@@ -126,7 +126,7 @@
}
}
- def make_file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
+ def make_file_content(buffer: Buffer): Bytes = (new File_Content_Request(buffer)).content()
/* theory text edits */
--- a/src/Tools/jEdit/src/main_plugin.scala Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Mon Dec 26 19:13:37 2022 +0100
@@ -110,7 +110,7 @@
private def delay_load_body(): Unit = {
val required_files = {
- val models = Document_Model.get_models()
+ val models = Document_Model.get_models_map()
val thy_files =
resources.resolve_dependencies(models.values, PIDE.editor.document_required())
@@ -124,7 +124,7 @@
}
else Nil
- (thy_files ::: aux_files).filterNot(models.isDefinedAt)
+ (thy_files ::: aux_files).filterNot(models.keySet)
}
if (required_files.nonEmpty) {
try {