support for generic File_Format.parse_data, with persistent result in document model;

--- 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,

--- 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))
   }
 

--- 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 */
 

--- 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 */

--- 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 */