--- a/src/Pure/GUI/gui.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Pure/GUI/gui.scala Tue Dec 27 22:52:28 2022 +0100
@@ -153,9 +153,7 @@
}
private def make_entries[A](batches: List[List[Entry[A]]]): List[Entry[A]] = {
- val item_batches =
- batches.map(_.flatMap(
- { case item: Item[_] => Some(item.asInstanceOf[Item[A]]) case _ => None }))
+ val item_batches = batches.map(_.flatMap(Library.as_subclass(classOf[Item[A]])))
val sep_entries: List[Entry[A]] =
item_batches.filter(_.nonEmpty).zipWithIndex.flatMap({ case (batch, i) =>
Separator[A](i) :: batch.map(_.copy(batch = i))
--- a/src/Pure/PIDE/document.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Pure/PIDE/document.scala Tue Dec 27 22:52:28 2022 +0100
@@ -796,7 +796,9 @@
def node_required: Boolean
def get_blob: Option[Blob]
- def bibtex_entries: Bibtex.Entries
+
+ def untyped_data: AnyRef
+ def get_data[C](c: Class[C]): Option[C] = Library.as_subclass(c)(untyped_data)
def node_edits(
node_header: Node.Header,
--- a/src/Pure/PIDE/editor.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Pure/PIDE/editor.scala Tue Dec 27 22:52:28 2022 +0100
@@ -8,12 +8,24 @@
abstract class Editor[Context] {
- /* session */
+ /* PIDE session and document model */
def session: Session
def flush(): Unit
def invoke(): Unit
+ def get_models(): Iterable[Document.Model]
+
+
+ /* bibtex */
+
+ def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document.Model)]] =
+ Bibtex.Entries.iterator(get_models())
+
+ def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
+ : Option[Completion.Result] =
+ Bibtex.completion(history, rendering, caret, get_models())
+
/* document editor */
--- a/src/Pure/PIDE/session.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Pure/PIDE/session.scala Tue Dec 27 22:52:28 2022 +0100
@@ -356,10 +356,7 @@
private val protocol_handlers = Protocol_Handlers.init(session)
def get_protocol_handler[C <: Session.Protocol_Handler](c: Class[C]): Option[C] =
- protocol_handlers.get(c.getName) match {
- case Some(h) if Library.is_subclass(h.getClass, c) => Some(h.asInstanceOf[C])
- case _ => None
- }
+ protocol_handlers.get(c.getName).flatMap(Library.as_subclass(c))
def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
protocol_handlers.init(handler)
--- a/src/Pure/Thy/bibtex.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Pure/Thy/bibtex.scala Tue Dec 27 22:52:28 2022 +0100
@@ -21,6 +21,9 @@
val format_name: String = "bibtex"
val file_ext: String = "bib"
+ override def parse_data(name: String, text: String): Bibtex.Entries =
+ Bibtex.Entries.parse(text, file_pos = name)
+
override def theory_suffix: String = "bibtex_file"
override def theory_content(name: String): String =
"""theory "bib" imports Pure begin bibtex_file """ +
@@ -192,11 +195,14 @@
def iterator[A <: Document.Model](models: Iterable[A]): Iterator[Text.Info[(String, A)]] =
for {
model <- models.iterator
- info <- model.bibtex_entries.entries.iterator
+ bibtex_entries <- model.get_data(classOf[Entries]).iterator
+ info <- bibtex_entries.entries.iterator
} yield info.map((_, model))
}
final class Entries private(val entries: List[Text.Info[String]], val errors: List[String]) {
+ override def toString: String = "Bibtex.Entries(" + entries.length + ")"
+
def ::: (other: Entries): Entries =
new Entries(entries ::: other.entries, errors ::: other.errors)
}
--- a/src/Pure/Thy/file_format.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Pure/Thy/file_format.scala Tue Dec 27 22:52:28 2022 +0100
@@ -8,6 +8,10 @@
object File_Format {
+ object No_Data extends AnyRef {
+ override def toString: String = "File_Format.No_Data"
+ }
+
sealed case class Theory_Context(name: Document.Node.Name, content: String)
@@ -24,6 +28,13 @@
def get_theory(name: Document.Node.Name): Option[File_Format] = get(name.theory)
def is_theory(name: Document.Node.Name): Boolean = get_theory(name).isDefined
+ def parse_data(name: String, text: String): AnyRef =
+ get(name) match {
+ case Some(file_format) => file_format.parse_data(name, text)
+ case None => No_Data
+ }
+ def parse_data(name: Document.Node.Name, text: String): AnyRef = parse_data(name.node, text)
+
def start_session(session: isabelle.Session): Session =
new Session(file_formats.map(_.start(session)).filterNot(_ == No_Agent))
}
@@ -56,6 +67,8 @@
def file_ext: String
def detect(name: String): Boolean = name.endsWith("." + file_ext)
+ def parse_data(name: String, text: String): AnyRef = File_Format.No_Data
+
/* implicit theory context: name and content */
--- a/src/Pure/Thy/sessions.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Pure/Thy/sessions.scala Tue Dec 27 22:52:28 2022 +0100
@@ -1100,8 +1100,7 @@
def parse_root(path: Path): List[Entry] = Parsers.parse_root(path)
def parse_root_entries(path: Path): List[Session_Entry] =
- for (entry <- Parsers.parse_root(path) if entry.isInstanceOf[Session_Entry])
- yield entry.asInstanceOf[Session_Entry]
+ Parsers.parse_root(path).flatMap(Library.as_subclass(classOf[Session_Entry]))
def parse_roots(roots: Path): List[String] = {
for {
--- a/src/Pure/library.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Pure/library.scala Tue Dec 27 22:52:28 2022 +0100
@@ -291,4 +291,7 @@
}
subclass(a)
}
+
+ def as_subclass[C](c: Class[C])(x: AnyRef): Option[C] =
+ if (x == null || is_subclass(x.getClass, c)) Some(x.asInstanceOf[C]) else None
}
--- a/src/Tools/VSCode/src/language_server.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Tools/VSCode/src/language_server.scala Tue Dec 27 22:52:28 2022 +0100
@@ -480,12 +480,14 @@
/* abstract editor operations */
object editor extends Language_Server.Editor {
- /* session */
+ /* PIDE session and document model */
override def session: Session = server.session
override def flush(): Unit = resources.flush_input(session, channel)
override def invoke(): Unit = delay_input.invoke()
+ override def get_models(): Iterable[Document.Model] = resources.get_models()
+
/* current situation */
--- a/src/Tools/VSCode/src/vscode_model.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Tools/VSCode/src/vscode_model.scala Tue Dec 27 22:52:28 2022 +0100
@@ -34,7 +34,7 @@
lazy val bytes: Bytes = Bytes(Symbol.encode(text))
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
- lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text, file_pos = node_name.node)
+ lazy val data: AnyRef = File_Format.registry.parse_data(node_name, text)
def recode_symbols: List[LSP.TextEdit] =
(for {
@@ -147,9 +147,9 @@
else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
- /* bibtex entries */
+ /* data */
- def bibtex_entries: Bibtex.Entries = model.content.bibtex_entries
+ def untyped_data: AnyRef = model.content.data
/* edits */
--- a/src/Tools/VSCode/src/vscode_rendering.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Tue Dec 27 22:52:28 2022 +0100
@@ -75,15 +75,6 @@
override def get_text(range: Text.Range): Option[String] = model.get_text(range)
- /* bibtex */
-
- def bibtex_entries_iterator(): Iterator[Text.Info[(String, VSCode_Model)]] =
- 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())
-
-
/* completion */
def completion(node_pos: Line.Node_Position, caret: Text.Offset): List[LSP.CompletionItem] = {
@@ -114,7 +105,7 @@
syntax_completion,
VSCode_Spell_Checker.completion(rendering, caret),
path_completion(caret),
- bibtex_completion(history, caret))
+ model.editor.bibtex_completion(history, rendering, caret))
val items =
results match {
case None => Nil
@@ -323,7 +314,8 @@
case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
val iterator =
for {
- Text.Info(entry_range, (entry, model)) <- bibtex_entries_iterator()
+ Text.Info(entry_range, (entry, model: VSCode_Model)) <-
+ model.editor.bibtex_entries_iterator()
if entry == name
} yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
if (iterator.isEmpty) None else Some(iterator.foldLeft(links)(_ :+ _))
--- a/src/Tools/jEdit/src/completion_popup.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Tools/jEdit/src/completion_popup.scala Tue Dec 27 22:52:28 2022 +0100
@@ -122,7 +122,7 @@
Completion.Result.merge(Completion.History.empty,
syntax_completion(Completion.History.empty, true, Some(rendering)),
rendering.path_completion(caret),
- Document_Model.bibtex_completion(Completion.History.empty, rendering, caret))
+ PIDE.editor.bibtex_completion(Completion.History.empty, rendering, caret))
.map(_.range)
rendering.semantic_completion(range0, range) match {
case None => range0
@@ -304,7 +304,7 @@
result1,
JEdit_Spell_Checker.completion(rendering, explicit, caret),
rendering.path_completion(caret),
- Document_Model.bibtex_completion(history, rendering, caret))
+ PIDE.editor.bibtex_completion(history, rendering, caret))
}
}
result match {
--- a/src/Tools/jEdit/src/document_model.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Tools/jEdit/src/document_model.scala Tue Dec 27 22:52:28 2022 +0100
@@ -32,8 +32,8 @@
def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
for {
(node_name, model) <- models.iterator
- if model.isInstanceOf[File_Model]
- } yield (node_name, model.asInstanceOf[File_Model])
+ file_model <- Library.as_subclass(classOf[File_Model])(model)
+ } yield (node_name, file_model)
def document_blobs: Document.Blobs =
Document.Blobs(
@@ -53,7 +53,7 @@
case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
case _ => None
}
- val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model)
+ val buffer_model = Buffer_Model.init(old_model, session, node_name, buffer)
(buffer_model,
copy(models = models + (node_name -> buffer_model),
buffer_models = buffer_models + (buffer -> buffer_model)))
@@ -100,16 +100,6 @@
def get_snapshot(buffer: JEditBuffer): Option[Document.Snapshot] = get_model(buffer).map(snapshot)
- /* bibtex */
-
- def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
- Bibtex.Entries.iterator(get_models())
-
- def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
- : Option[Completion.Result] =
- Bibtex.completion(history, rendering, caret, get_models())
-
-
/* overlays */
def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
@@ -300,7 +290,7 @@
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: Bibtex.Entries = Bibtex.Entries.parse(text, file_pos = node_name.node)
+ lazy val data: AnyRef = File_Format.registry.parse_data(node_name, text)
}
@@ -446,8 +436,7 @@
if (is_theory) None
else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
- def bibtex_entries: Bibtex.Entries =
- if (File.is_bib(node_name.node)) content.bibtex_entries else Bibtex.Entries.empty
+ def untyped_data: AnyRef = content.data
/* edits */
@@ -485,8 +474,20 @@
def is_stable: Boolean = pending_edits.isEmpty
}
-case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
-extends Document_Model {
+object Buffer_Model {
+ def init(
+ old_model: Option[File_Model],
+ session: Session,
+ node_name: Document.Node.Name,
+ buffer: Buffer
+ ): Buffer_Model = (new Buffer_Model(session, node_name, buffer)).init(old_model)
+}
+
+class Buffer_Model private(
+ val session: Session,
+ val node_name: Document.Node.Name,
+ val buffer: Buffer
+) extends Document_Model {
/* text */
def get_text(range: Text.Range): Option[String] =
@@ -556,7 +557,7 @@
def edit(edits: List[Text.Edit]): Unit = GUI_Thread.require {
reset_blob()
- reset_bibtex_entries()
+ reset_data()
for (doc_view <- document_view_iterator) {
doc_view.rich_text_area.active_reset()
@@ -591,23 +592,19 @@
}
- // bibtex entries
+ // parsed data
- private var bibtex_entries: Option[Bibtex.Entries] = None
+ private var data: Option[AnyRef] = None
- def reset_bibtex_entries(): Unit = GUI_Thread.require { bibtex_entries = None }
+ def reset_data(): Unit = GUI_Thread.require { data = 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
- }
+ def untyped_data: AnyRef = GUI_Thread.require {
+ data getOrElse {
+ val text = JEdit_Lib.buffer_text(buffer)
+ val res = File_Format.registry.parse_data(node_name, text)
+ data = Some(res)
+ res
}
- else Bibtex.Entries.empty
}
}
@@ -620,8 +617,7 @@
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
+ def untyped_data: AnyRef = buffer_state.untyped_data
/* buffer listener */
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Dec 27 22:52:28 2022 +0100
@@ -18,7 +18,7 @@
class JEdit_Editor extends Editor[View] {
- /* session */
+ /* PIDE session and document model */
override def session: Session = PIDE.session
@@ -53,6 +53,9 @@
} yield doc_view.model.node_name).contains(name)
+ override def get_models(): Iterable[Document.Model] = Document_Model.get_models()
+
+
/* global changes */
def state_changed(): Unit = {
--- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Dec 27 10:38:34 2022 +0000
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Tue Dec 27 22:52:28 2022 +0100
@@ -272,8 +272,8 @@
case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
val opt_link =
- Document_Model.bibtex_entries_iterator().collectFirst(
- { case Text.Info(entry_range, (entry, model)) if entry == name =>
+ PIDE.editor.bibtex_entries_iterator().collectFirst(
+ { case Text.Info(entry_range, (entry, model: Document_Model)) if entry == name =>
PIDE.editor.hyperlink_model(true, model, entry_range.start) })
opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))