# HG changeset patch # User wenzelm # Date 1672177948 -3600 # Node ID 04af11e6557a84cb432b8da2b5422caad34e60e9 # Parent 7fd705b107f2b9c7cb87192b68d138f62c225d5f# Parent 941d4f5270916b75178551b91056c78405598fee merged diff -r 7fd705b107f2 -r 04af11e6557a src/Pure/GUI/gui.scala --- 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)) diff -r 7fd705b107f2 -r 04af11e6557a src/Pure/PIDE/document.scala --- 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, diff -r 7fd705b107f2 -r 04af11e6557a src/Pure/PIDE/editor.scala --- 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 */ diff -r 7fd705b107f2 -r 04af11e6557a src/Pure/PIDE/session.scala --- 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) diff -r 7fd705b107f2 -r 04af11e6557a src/Pure/Thy/bibtex.scala --- 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) } diff -r 7fd705b107f2 -r 04af11e6557a src/Pure/Thy/file_format.scala --- 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 */ diff -r 7fd705b107f2 -r 04af11e6557a src/Pure/Thy/sessions.scala --- 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 { diff -r 7fd705b107f2 -r 04af11e6557a src/Pure/library.scala --- 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 } diff -r 7fd705b107f2 -r 04af11e6557a src/Tools/VSCode/src/language_server.scala --- 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 */ diff -r 7fd705b107f2 -r 04af11e6557a src/Tools/VSCode/src/vscode_model.scala --- 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 */ diff -r 7fd705b107f2 -r 04af11e6557a src/Tools/VSCode/src/vscode_rendering.scala --- 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)(_ :+ _)) diff -r 7fd705b107f2 -r 04af11e6557a src/Tools/jEdit/src/completion_popup.scala --- 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 { diff -r 7fd705b107f2 -r 04af11e6557a src/Tools/jEdit/src/document_model.scala --- 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 */ diff -r 7fd705b107f2 -r 04af11e6557a src/Tools/jEdit/src/jedit_editor.scala --- 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 = { diff -r 7fd705b107f2 -r 04af11e6557a src/Tools/jEdit/src/jedit_rendering.scala --- 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))