14 import scala.util.parsing.input.Reader |
14 import scala.util.parsing.input.Reader |
15 |
15 |
16 |
16 |
17 object Bibtex |
17 object Bibtex |
18 { |
18 { |
|
19 /** file format **/ |
|
20 |
|
21 def is_bibtex(name: String): Boolean = name.endsWith(".bib") |
|
22 |
|
23 class File_Format extends isabelle.File_Format |
|
24 { |
|
25 val format_name: String = "bibtex" |
|
26 val node_suffix: String = "bibtex_file" |
|
27 |
|
28 def detect(name: String): Boolean = is_bibtex(name) |
|
29 |
|
30 override def make_theory_name( |
|
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 |
|
49 override def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = |
|
50 { |
|
51 val name = snapshot.node_name |
|
52 if (detect(name.node)) { |
|
53 val title = "Bibliography " + quote(snapshot.node_name.path.base_name) |
|
54 val content = |
|
55 Isabelle_System.with_tmp_file("bib", "bib") { bib => |
|
56 File.write(bib, snapshot.node.source) |
|
57 Bibtex.html_output(List(bib), style = "unsort", title = title) |
|
58 } |
|
59 Some(Present.Preview(title, content)) |
|
60 } |
|
61 else None |
|
62 } |
|
63 } |
|
64 |
|
65 |
|
66 |
19 /** bibtex errors **/ |
67 /** bibtex errors **/ |
20 |
68 |
21 def bibtex_errors(dir: Path, root_name: String): List[String] = |
69 def bibtex_errors(dir: Path, root_name: String): List[String] = |
22 { |
70 { |
23 val log_path = dir + Path.explode(root_name).ext("blg") |
71 val log_path = dir + Path.explode(root_name).ext("blg") |
119 } |
167 } |
120 |
168 |
121 |
169 |
122 |
170 |
123 /** document model **/ |
171 /** document model **/ |
124 |
|
125 /* bibtex files */ |
|
126 |
|
127 def is_bibtex(name: String): Boolean = name.endsWith(".bib") |
|
128 |
|
129 private val node_suffix: String = "bibtex_file" |
|
130 |
|
131 def make_theory_name(resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] = |
|
132 { |
|
133 Thy_Header.file_name(name.node) match { |
|
134 case Some(bib_name) if is_bibtex(bib_name) => |
|
135 val thy_node = resources.append(name.node, Path.explode(node_suffix)) |
|
136 Some(Document.Node.Name(thy_node, name.master_dir, bib_name)) |
|
137 case _ => None |
|
138 } |
|
139 } |
|
140 |
|
141 def make_theory_content(bib_name: String): Option[String] = |
|
142 if (is_bibtex(bib_name)) { |
|
143 Some("""theory "bib" imports Pure begin bibtex_file """ + quote(bib_name) + """ end""") |
|
144 } |
|
145 else None |
|
146 |
|
147 def make_theory_content(file: JFile): Option[String] = |
|
148 if (file.getName == node_suffix) { |
|
149 val parent = file.getParentFile |
|
150 if (parent != null && is_bibtex(parent.getName)) make_theory_content(parent.getName) |
|
151 else None |
|
152 } |
|
153 else None |
|
154 |
|
155 |
172 |
156 /* entries */ |
173 /* entries */ |
157 |
174 |
158 def entries(text: String): List[Text.Info[String]] = |
175 def entries(text: String): List[Text.Info[String]] = |
159 { |
176 { |