# HG changeset patch
# User wenzelm
# Date 1541626316 -3600
# Node ID 039edba27102dfd69f2ae5ad820882a313f1430c
# Parent  c78c95d2a3d1beaad7489d2c198b8ed557ad4a66
clarified signature;

diff -r c78c95d2a3d1 -r 039edba27102 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Wed Nov 07 22:15:03 2018 +0100
+++ b/src/Pure/Thy/bibtex.scala	Wed Nov 07 22:31:56 2018 +0100
@@ -23,28 +23,11 @@
   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)
+    val file_ext: String = "bib"
 
-    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 theory_suffix: String = "bibtex_file"
+    override def theory_content(ext_name: String): String =
+      """theory "bib" imports Pure begin bibtex_file """ + quote(ext_name) + """ end"""
 
     override def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
     {
diff -r c78c95d2a3d1 -r 039edba27102 src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Wed Nov 07 22:15:03 2018 +0100
+++ b/src/Pure/Thy/file_format.scala	Wed Nov 07 22:31:56 2018 +0100
@@ -44,13 +44,35 @@
   def format_name: String
   override def toString = format_name
 
-  def detect(name: String): Boolean
+  def file_ext: String
+  def detect(name: String): Boolean = name.endsWith("." + file_ext)
+
+
+  /* implicit theory context: name and content */
+
+  def theory_suffix: String = ""
+  def theory_content(ext_name: String): String = ""
 
-  def make_theory_name(
-    resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] = None
+  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) && theory_suffix.nonEmpty
+    }
+    yield {
+      val thy_node = resources.append(name.node, Path.explode(theory_suffix))
+      Document.Node.Name(thy_node, name.master_dir, ext_name)
+    }
+  }
 
-  def make_theory_content(
-    resources: Resources, thy_name: Document.Node.Name): Option[String] = None
+  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 == theory_suffix
+      (_, ext_name) <- Thy_Header.split_file_name(prefix) if detect(ext_name)
+      s <- proper_string(theory_content(ext_name))
+    } yield s
+  }
 
   def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = None
 }