clarified signature;
authorwenzelm
Wed Nov 07 22:31:56 2018 +0100 (6 months ago)
changeset 69257039edba27102
parent 69256 c78c95d2a3d1
child 69258 e05c9f314f90
clarified signature;
src/Pure/Thy/bibtex.scala
src/Pure/Thy/file_format.scala
     1.1 --- a/src/Pure/Thy/bibtex.scala	Wed Nov 07 22:15:03 2018 +0100
     1.2 +++ b/src/Pure/Thy/bibtex.scala	Wed Nov 07 22:31:56 2018 +0100
     1.3 @@ -23,28 +23,11 @@
     1.4    class File_Format extends isabelle.File_Format
     1.5    {
     1.6      val format_name: String = "bibtex"
     1.7 -    val node_suffix: String = "bibtex_file"
     1.8 -
     1.9 -    def detect(name: String): Boolean = is_bibtex(name)
    1.10 +    val file_ext: String = "bib"
    1.11  
    1.12 -    override def make_theory_name(
    1.13 -      resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
    1.14 -    {
    1.15 -      for { (_, ext_name) <- Thy_Header.split_file_name(name.node) if detect(ext_name) }
    1.16 -      yield {
    1.17 -        val thy_node = resources.append(name.node, Path.explode(node_suffix))
    1.18 -        Document.Node.Name(thy_node, name.master_dir, ext_name)
    1.19 -      }
    1.20 -    }
    1.21 -
    1.22 -    override def make_theory_content(
    1.23 -      resources: Resources, thy_name: Document.Node.Name): Option[String] =
    1.24 -    {
    1.25 -      for {
    1.26 -        (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node) if suffix == node_suffix
    1.27 -        (_, ext_name) <- Thy_Header.split_file_name(prefix) if detect(ext_name)
    1.28 -      } yield """theory "bib" imports Pure begin bibtex_file """ + quote(ext_name) + """ end"""
    1.29 -    }
    1.30 +    override def theory_suffix: String = "bibtex_file"
    1.31 +    override def theory_content(ext_name: String): String =
    1.32 +      """theory "bib" imports Pure begin bibtex_file """ + quote(ext_name) + """ end"""
    1.33  
    1.34      override def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
    1.35      {
     2.1 --- a/src/Pure/Thy/file_format.scala	Wed Nov 07 22:15:03 2018 +0100
     2.2 +++ b/src/Pure/Thy/file_format.scala	Wed Nov 07 22:31:56 2018 +0100
     2.3 @@ -44,13 +44,35 @@
     2.4    def format_name: String
     2.5    override def toString = format_name
     2.6  
     2.7 -  def detect(name: String): Boolean
     2.8 +  def file_ext: String
     2.9 +  def detect(name: String): Boolean = name.endsWith("." + file_ext)
    2.10 +
    2.11 +
    2.12 +  /* implicit theory context: name and content */
    2.13 +
    2.14 +  def theory_suffix: String = ""
    2.15 +  def theory_content(ext_name: String): String = ""
    2.16  
    2.17 -  def make_theory_name(
    2.18 -    resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] = None
    2.19 +  def make_theory_name(resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
    2.20 +  {
    2.21 +    for {
    2.22 +      (_, ext_name) <- Thy_Header.split_file_name(name.node)
    2.23 +      if detect(ext_name) && theory_suffix.nonEmpty
    2.24 +    }
    2.25 +    yield {
    2.26 +      val thy_node = resources.append(name.node, Path.explode(theory_suffix))
    2.27 +      Document.Node.Name(thy_node, name.master_dir, ext_name)
    2.28 +    }
    2.29 +  }
    2.30  
    2.31 -  def make_theory_content(
    2.32 -    resources: Resources, thy_name: Document.Node.Name): Option[String] = None
    2.33 +  def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] =
    2.34 +  {
    2.35 +    for {
    2.36 +      (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node) if suffix == theory_suffix
    2.37 +      (_, ext_name) <- Thy_Header.split_file_name(prefix) if detect(ext_name)
    2.38 +      s <- proper_string(theory_content(ext_name))
    2.39 +    } yield s
    2.40 +  }
    2.41  
    2.42    def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = None
    2.43  }