# HG changeset patch
# User wenzelm
# Date 1541623336 -3600
# Node ID 800b1ce96fce617ffe3000ac489789896346aaa5
# Parent  9f8d26b8c7317344fa1f0333585b41e51911d310
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;

diff -r 9f8d26b8c731 -r 800b1ce96fce etc/settings
--- a/etc/settings	Wed Nov 07 14:06:43 2018 +0100
+++ b/etc/settings	Wed Nov 07 21:42:16 2018 +0100
@@ -20,6 +20,8 @@
 
 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
 
+isabelle_file_format 'isabelle.Bibtex$File_Format'
+
 #paranoia settings -- avoid intrusion of alien options
 unset "_JAVA_OPTIONS"
 unset "JAVA_TOOL_OPTIONS"
diff -r 9f8d26b8c731 -r 800b1ce96fce lib/scripts/getfunctions
--- a/lib/scripts/getfunctions	Wed Nov 07 14:06:43 2018 +0100
+++ b/lib/scripts/getfunctions	Wed Nov 07 21:42:16 2018 +0100
@@ -109,6 +109,22 @@
 }
 export -f classpath
 
+#file formats
+function isabelle_file_format ()
+{
+  local X=""
+  for X in "$@"
+  do
+    if [ -z "$ISABELLE_CLASSES_FILE_FORMAT" ]; then
+      ISABELLE_CLASSES_FILE_FORMAT="$X"
+    else
+      ISABELLE_CLASSES_FILE_FORMAT="$ISABELLE_CLASSES_FILE_FORMAT:$X"
+    fi
+  done
+  export ISABELLE_CLASSES_FILE_FORMAT
+}
+export -f isabelle_file_format
+
 #administrative build
 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   function isabelle_admin_build ()
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -119,9 +119,6 @@
 
       def path: Path = Path.explode(File.standard_path(node))
 
-      def is_bibtex: Boolean = Bibtex.is_bibtex(node)
-      def is_bibtex_theory: Boolean = Bibtex.is_bibtex(theory)
-
       def is_theory: Boolean = theory.nonEmpty
 
       def theory_base_name: String = Long_Name.base_name(theory)
@@ -586,8 +583,6 @@
 
     def node_required: Boolean
     def get_blob: Option[Blob]
-    def is_bibtex: Boolean = node_name.is_bibtex
-    def is_bibtex_theory: Boolean = node_name.is_bibtex_theory
     def bibtex_entries: List[Text.Info[String]]
 
     def node_edits(
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Pure/PIDE/document_status.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -248,7 +248,7 @@
       }
 
     def update(
-      session_base: Sessions.Base,
+      resources: Resources,
       state: Document.State,
       version: Document.Version,
       domain: Option[Set[Document.Node.Name]] = None,
@@ -258,8 +258,8 @@
       val update_iterator =
         for {
           name <- domain.getOrElse(nodes1.domain).iterator
-          if !Sessions.is_hidden(name) &&
-              !session_base.loaded_theory(name) &&
+          if !resources.is_hidden(name) &&
+              !resources.session_base.loaded_theory(name) &&
               !nodes1.is_suppressed(name) &&
               !nodes1(name).is_empty
           st = Document_Status.Node_Status.make(state, version, name)
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Pure/PIDE/headless.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -263,7 +263,7 @@
                       else changed.nodes.iterator.filter(dep_theories_set).toSet
 
                     val (nodes_status_changed, nodes_status1) =
-                      st.nodes_status.update(resources.session_base, state, version,
+                      st.nodes_status.update(resources, state, version,
                         domain = Some(domain), trim = changed.assignment)
 
                     if (nodes_status_delay >= Time.zero && nodes_status_changed) {
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Pure/PIDE/resources.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -19,6 +19,23 @@
 {
   resources =>
 
+
+  /* file formats */
+
+  val file_formats: File_Format.Environment = File_Format.environment()
+
+  def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] =
+    file_formats.get(name).flatMap(_.make_theory_name(resources, name))
+
+  def make_theory_content(thy_name: Document.Node.Name): Option[String] =
+    file_formats.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
+
+  def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
+    file_formats.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
+
+  def is_hidden(name: Document.Node.Name): Boolean =
+    !name.is_theory || name.theory == Sessions.root_name || file_formats.is_theory(name)
+
   def thy_path(path: Path): Path = path.ext("thy")
 
 
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Pure/Thy/bibtex.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -16,6 +16,54 @@
 
 object Bibtex
 {
+  /** file format **/
+
+  def is_bibtex(name: String): Boolean = name.endsWith(".bib")
+
+  class File_Format extends isabelle.File_Format
+  {
+    val format_name: String = "bibtex"
+    val node_suffix: String = "bibtex_file"
+
+    def detect(name: String): Boolean = is_bibtex(name)
+
+    override def make_theory_name(
+      resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
+    {
+      for { (_, ext_name) <- Thy_Header.split_file_name(name.node) if detect(ext_name) }
+      yield {
+        val thy_node = resources.append(name.node, Path.explode(node_suffix))
+        Document.Node.Name(thy_node, name.master_dir, ext_name)
+      }
+    }
+
+    override def make_theory_content(
+      resources: Resources, thy_name: Document.Node.Name): Option[String] =
+    {
+      for {
+        (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node) if suffix == node_suffix
+        (_, ext_name) <- Thy_Header.split_file_name(prefix) if detect(ext_name)
+      } yield """theory "bib" imports Pure begin bibtex_file """ + quote(ext_name) + """ end"""
+    }
+
+    override def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
+    {
+      val name = snapshot.node_name
+      if (detect(name.node)) {
+        val title = "Bibliography " + quote(snapshot.node_name.path.base_name)
+        val content =
+          Isabelle_System.with_tmp_file("bib", "bib") { bib =>
+            File.write(bib, snapshot.node.source)
+            Bibtex.html_output(List(bib), style = "unsort", title = title)
+          }
+        Some(Present.Preview(title, content))
+      }
+      else None
+    }
+  }
+
+
+
   /** bibtex errors **/
 
   def bibtex_errors(dir: Path, root_name: String): List[String] =
@@ -122,37 +170,6 @@
 
   /** document model **/
 
-  /* bibtex files */
-
-  def is_bibtex(name: String): Boolean = name.endsWith(".bib")
-
-  private val node_suffix: String = "bibtex_file"
-
-  def make_theory_name(resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
-  {
-    Thy_Header.file_name(name.node) match {
-      case Some(bib_name) if is_bibtex(bib_name) =>
-        val thy_node = resources.append(name.node, Path.explode(node_suffix))
-        Some(Document.Node.Name(thy_node, name.master_dir, bib_name))
-      case _ => None
-    }
-  }
-
-  def make_theory_content(bib_name: String): Option[String] =
-    if (is_bibtex(bib_name)) {
-      Some("""theory "bib" imports Pure begin bibtex_file """ + quote(bib_name) + """ end""")
-    }
-    else None
-
-  def make_theory_content(file: JFile): Option[String] =
-    if (file.getName == node_suffix) {
-      val parent = file.getParentFile
-      if (parent != null && is_bibtex(parent.getName)) make_theory_content(parent.getName)
-      else None
-    }
-    else None
-
-
   /* entries */
 
   def entries(text: String): List[Text.Info[String]] =
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Pure/Thy/file_format.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/file_format.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -0,0 +1,56 @@
+/*  Title:      Pure/Thy/file_format.scala
+    Author:     Makarius
+
+Support for user-defined file formats.
+*/
+
+package isabelle
+
+
+object File_Format
+{
+  def environment(): Environment =
+  {
+    val file_formats =
+      for (name <- space_explode(':', Isabelle_System.getenv_strict("ISABELLE_CLASSES_FILE_FORMAT")))
+      yield {
+        def err(msg: String): Nothing =
+          error("Bad entry " + quote(name) + " in ISABELLE_CLASSES_FILE_FORMAT\n" + msg)
+
+        try { Class.forName(name).asInstanceOf[Class[File_Format]].newInstance() }
+        catch {
+          case _: ClassNotFoundException => err("Class not found")
+          case exn: Throwable => err(Exn.message(exn))
+        }
+      }
+    new Environment(file_formats)
+  }
+
+  final class Environment private [File_Format](file_formats: List[File_Format])
+  {
+    override def toString: String = file_formats.mkString("File_Format.Environment(", ",", ")")
+
+    def get(name: String): Option[File_Format] = file_formats.find(_.detect(name))
+    def get(name: Document.Node.Name): Option[File_Format] = get(name.node)
+    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
+  }
+
+  sealed case class Theory_Context(name: Document.Node.Name, content: String)
+}
+
+trait File_Format
+{
+  def format_name: String
+  override def toString = format_name
+
+  def detect(name: String): Boolean
+
+  def make_theory_name(
+    resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] = None
+
+  def make_theory_content(
+    resources: Resources, thy_name: Document.Node.Name): Option[String] = None
+
+  def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = None
+}
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Pure/Thy/present.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -105,7 +105,9 @@
 
   sealed case class Preview(title: String, content: String)
 
-  def preview(snapshot: Document.Snapshot,
+  def preview(
+    resources: Resources,
+    snapshot: Document.Snapshot,
     plain_text: Boolean = false,
     fonts_url: String => String = HTML.fonts_url()): Preview =
   {
@@ -119,26 +121,22 @@
         List(HTML.source(body)), css = "", structural = false)
 
     val name = snapshot.node_name
+
     if (plain_text) {
       val title = "File " + quote(name.path.base_name)
       val content = output_document(title, HTML.text(snapshot.node.source))
       Preview(title, content)
     }
-    else if (name.is_bibtex) {
-      val title = "Bibliography " + quote(name.path.base_name)
-      val content =
-        Isabelle_System.with_tmp_file("bib", "bib") { bib =>
-          File.write(bib, snapshot.node.source)
-          Bibtex.html_output(List(bib), style = "unsort", title = title)
-        }
-      Preview(title, content)
-    }
     else {
-      val title =
-        if (name.is_theory) "Theory " + quote(name.theory_base_name)
-        else "File " + quote(name.path.base_name)
-      val content = output_document(title, pide_document(snapshot))
-      Preview(title, content)
+      resources.make_preview(snapshot) match {
+        case Some(preview) => preview
+        case None =>
+          val title =
+            if (name.is_theory) "Theory " + quote(name.theory_base_name)
+            else "File " + quote(name.path.base_name)
+          val content = output_document(title, pide_document(snapshot))
+          Preview(title, content)
+      }
     }
   }
 
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -26,9 +26,6 @@
 
   def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
-  def is_hidden(name: Document.Node.Name): Boolean =
-    !name.is_theory || name.theory == Sessions.root_name || name.is_bibtex_theory
-
 
   def exclude_session(name: String): Boolean = name == "" || name == DRAFT
 
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Pure/Thy/thy_header.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -80,14 +80,15 @@
     (Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE)
 
   private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
+  private val Split_File_Name = new Regex("""(.*?)[/\\]*([^/\\:]+)""")
   private val File_Name = new Regex(""".*?([^/\\:]+)""")
 
   def is_base_name(s: String): Boolean =
     s != "" && !s.exists("/\\:".contains(_))
 
-  def file_name(s: String): Option[String] =
+  def split_file_name(s: String): Option[(String, String)] =
     s match {
-      case File_Name(s) => Some(s)
+      case Split_File_Name(s1, s2) => Some((s1, s2))
       case _ => None
     }
 
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Pure/build-jars	Wed Nov 07 21:42:16 2018 +0100
@@ -131,6 +131,7 @@
   Thy/bibtex.scala
   Thy/export.scala
   Thy/export_theory.scala
+  Thy/file_format.scala
   Thy/html.scala
   Thy/latex.scala
   Thy/present.scala
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -59,7 +59,7 @@
 
   def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
     Document_Model(session, editor, node_name, Content.empty,
-      node_required = node_name.is_bibtex_theory)
+      node_required = session.resources.file_formats.is_theory(node_name))
 }
 
 sealed case class Document_Model(
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Tools/VSCode/src/preview_panel.scala
--- a/src/Tools/VSCode/src/preview_panel.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -30,7 +30,7 @@
               val snapshot = model.snapshot()
               if (snapshot.is_outdated) m
               else {
-                val preview = Present.preview(snapshot)
+                val preview = Present.preview(resources, snapshot)
                 channel.write(
                   Protocol.Preview_Response(file, column, preview.title, preview.content))
                 m - file
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -123,10 +123,8 @@
 
   def read_file_content(file: JFile): Option[String] =
   {
-    Bibtex.make_theory_content(file) orElse {
-      try { Some(Line.normalize(File.read(file))) }
-      catch { case ERROR(_) => None }
-    }
+    try { Some(Line.normalize(File.read(file))) }
+    catch { case ERROR(_) => None }
   }
 
   def get_file_content(file: JFile): Option[String] =
@@ -226,8 +224,8 @@
 
         val thy_files2 =
           (for {
-            (_, model) <- st.models.iterator if model.node_name.is_bibtex
-            thy_name <- Bibtex.make_theory_name(resources, model.node_name)
+            (_, model) <- st.models.iterator
+            thy_name <- resources.make_theory_name(model.node_name)
           } yield thy_name).toList
 
 
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -320,7 +320,7 @@
         yield {
           val snapshot = model.await_stable_snapshot()
           val preview =
-            Present.preview(snapshot, fonts_url = HTML.fonts_dir(fonts_root),
+            Present.preview(PIDE.resources, snapshot, fonts_url = HTML.fonts_dir(fonts_root),
               plain_text = query.startsWith(plain_text_prefix))
           HTTP.Response.html(preview.content)
         })
@@ -389,7 +389,7 @@
     file.foreach(PIDE.plugin.file_watcher.register_parent(_))
 
     val content = Document_Model.File_Content(text)
-    val node_required1 = node_required || node_name.is_bibtex_theory
+    val node_required1 = node_required || session.resources.file_formats.is_theory(node_name)
     File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
   }
 }
@@ -427,7 +427,7 @@
     else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
 
   def bibtex_entries: List[Text.Info[String]] =
-    if (is_bibtex) content.bibtex_entries else Nil
+    if (Bibtex.is_bibtex(node_name.node)) content.bibtex_entries else Nil
 
 
   /* edits */
@@ -454,7 +454,7 @@
 
   def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
     if (pending_edits.nonEmpty ||
-        !is_bibtex_theory &&
+        !session.resources.file_formats.is_theory(node_name) &&
           (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
     else {
       val text_edits = List(Text.Edit.remove(0, content.text))
@@ -551,7 +551,7 @@
 
   def bibtex_entries: List[Text.Info[String]] =
     GUI_Thread.require {
-      if (is_bibtex) {
+      if (Bibtex.is_bibtex(node_name.node)) {
         _bibtex_entries match {
           case Some(entries) => entries
           case None =>
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -80,7 +80,7 @@
 
   def read_file_content(node_name: Document.Node.Name): Option[String] =
   {
-    Bibtex.make_theory_content(node_name.theory) orElse {
+    make_theory_content(node_name) orElse {
       val name = node_name.node
       try {
         val text =
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -131,8 +131,8 @@
 
           val thy_files2 =
             (for {
-              (name, _) <- models.iterator if name.is_bibtex
-              thy_name <- Bibtex.make_theory_name(resources, name)
+              (name, _) <- models.iterator
+              thy_name <- resources.make_theory_name(name)
             } yield thy_name).toList
 
           val aux_files =
diff -r 9f8d26b8c731 -r 800b1ce96fce src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -214,12 +214,11 @@
   {
     GUI_Thread.require {}
 
-    val session_base = PIDE.resources.session_base
     val snapshot = PIDE.session.snapshot()
 
     val (nodes_status_changed, nodes_status1) =
       nodes_status.update(
-        session_base, snapshot.state, snapshot.version, domain = domain, trim = trim)
+        PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
 
     nodes_status = nodes_status1
     if (nodes_status_changed) status.listData = nodes_status1.present.map(_._1)