src/Pure/Thy/bibtex.scala
changeset 69257 039edba27102
parent 69255 800b1ce96fce
child 69259 438e1a11445f
equal deleted inserted replaced
69256:c78c95d2a3d1 69257:039edba27102
    21   def is_bibtex(name: String): Boolean = name.endsWith(".bib")
    21   def is_bibtex(name: String): Boolean = name.endsWith(".bib")
    22 
    22 
    23   class File_Format extends isabelle.File_Format
    23   class File_Format extends isabelle.File_Format
    24   {
    24   {
    25     val format_name: String = "bibtex"
    25     val format_name: String = "bibtex"
    26     val node_suffix: String = "bibtex_file"
    26     val file_ext: String = "bib"
    27 
    27 
    28     def detect(name: String): Boolean = is_bibtex(name)
    28     override def theory_suffix: String = "bibtex_file"
    29 
    29     override def theory_content(ext_name: String): String =
    30     override def make_theory_name(
    30       """theory "bib" imports Pure begin bibtex_file """ + quote(ext_name) + """ end"""
    31       resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
       
    32     {
       
    33       for { (_, ext_name) <- Thy_Header.split_file_name(name.node) if detect(ext_name) }
       
    34       yield {
       
    35         val thy_node = resources.append(name.node, Path.explode(node_suffix))
       
    36         Document.Node.Name(thy_node, name.master_dir, ext_name)
       
    37       }
       
    38     }
       
    39 
       
    40     override def make_theory_content(
       
    41       resources: Resources, thy_name: Document.Node.Name): Option[String] =
       
    42     {
       
    43       for {
       
    44         (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node) if suffix == node_suffix
       
    45         (_, ext_name) <- Thy_Header.split_file_name(prefix) if detect(ext_name)
       
    46       } yield """theory "bib" imports Pure begin bibtex_file """ + quote(ext_name) + """ end"""
       
    47     }
       
    48 
    31 
    49     override def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
    32     override def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
    50     {
    33     {
    51       val name = snapshot.node_name
    34       val name = snapshot.node_name
    52       if (detect(name.node)) {
    35       if (detect(name.node)) {