# HG changeset patch # User wenzelm # Date 1672158901 -3600 # Node ID 23f433294173b2b089fe08d0d6f34fc7ddd1f9f8 # Parent c36d666ee5ee8f6b2e7bc5c8794b9da7dcf6cfec support for generic File_Format.parse_data, with persistent result in document model; diff -r c36d666ee5ee -r 23f433294173 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Dec 27 16:36:00 2022 +0100 +++ b/src/Pure/PIDE/document.scala Tue Dec 27 17:35:01 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 c36d666ee5ee -r 23f433294173 src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala Tue Dec 27 16:36:00 2022 +0100 +++ b/src/Pure/Thy/bibtex.scala Tue Dec 27 17:35:01 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,7 +195,8 @@ 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)) } diff -r c36d666ee5ee -r 23f433294173 src/Pure/Thy/file_format.scala --- a/src/Pure/Thy/file_format.scala Tue Dec 27 16:36:00 2022 +0100 +++ b/src/Pure/Thy/file_format.scala Tue Dec 27 17:35:01 2022 +0100 @@ -8,6 +8,8 @@ object File_Format { + object No_Data extends AnyRef + sealed case class Theory_Context(name: Document.Node.Name, content: String) @@ -24,6 +26,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 +65,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 c36d666ee5ee -r 23f433294173 src/Tools/VSCode/src/vscode_model.scala --- a/src/Tools/VSCode/src/vscode_model.scala Tue Dec 27 16:36:00 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_model.scala Tue Dec 27 17:35:01 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 c36d666ee5ee -r 23f433294173 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Tue Dec 27 16:36:00 2022 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Tue Dec 27 17:35:01 2022 +0100 @@ -300,7 +300,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 +446,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 */ @@ -568,7 +567,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() @@ -603,22 +602,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) - 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 } } @@ -631,8 +627,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 */