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