author | wenzelm |
Thu, 22 Sep 2022 17:24:50 +0200 | |
changeset 76204 | b80b2fbc46c3 |
parent 75941 | 4bbbbaa656f1 |
child 76776 | 011759a7f2f6 |
permissions | -rw-r--r-- |
67274 | 1 |
/* Title: Pure/Thy/bibtex.scala |
58523 | 2 |
Author: Makarius |
3 |
||
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58543
diff
changeset
|
4 |
BibTeX support. |
58523 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
67290 | 10 |
import java.io.{File => JFile} |
11 |
||
58528 | 12 |
import scala.collection.mutable |
58523 | 13 |
import scala.util.parsing.combinator.RegexParsers |
64824 | 14 |
import scala.util.parsing.input.Reader |
58523 | 15 |
|
16 |
||
75393 | 17 |
object Bibtex { |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
18 |
/** file format **/ |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
19 |
|
75393 | 20 |
class File_Format extends isabelle.File_Format { |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
21 |
val format_name: String = "bibtex" |
69257 | 22 |
val file_ext: String = "bib" |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
23 |
|
69257 | 24 |
override def theory_suffix: String = "bibtex_file" |
69259 | 25 |
override def theory_content(name: String): String = |
72836 | 26 |
"""theory "bib" imports Pure begin bibtex_file """ + |
27 |
Outer_Syntax.quote_string(name) + """ end""" |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
28 |
|
75941 | 29 |
override def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = { |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
30 |
val name = snapshot.node_name |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
31 |
if (detect(name.node)) { |
69366 | 32 |
val title = "Bibliography " + quote(snapshot.node_name.path.file_name) |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
33 |
val content = |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
34 |
Isabelle_System.with_tmp_file("bib", "bib") { bib => |
76204
b80b2fbc46c3
clarified signature: persistent Node.source / Snapshot.source;
wenzelm
parents:
75941
diff
changeset
|
35 |
File.write(bib, snapshot.source) |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
36 |
Bibtex.html_output(List(bib), style = "unsort", title = title) |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
37 |
} |
75941 | 38 |
Some(Browser_Info.HTML_Document(title, content)) |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
39 |
} |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
40 |
else None |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
41 |
} |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
42 |
} |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
43 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
44 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
68224
diff
changeset
|
45 |
|
67203 | 46 |
/** bibtex errors **/ |
47 |
||
75393 | 48 |
def bibtex_errors(dir: Path, root_name: String): List[String] = { |
67203 | 49 |
val log_path = dir + Path.explode(root_name).ext("blg") |
50 |
if (log_path.is_file) { |
|
67300 | 51 |
val Error1 = """^(I couldn't open database file .+)$""".r |
73730
2f023b2b0e1e
more uniform bibtex error, without using perl (see 4710dd5093a3);
wenzelm
parents:
73565
diff
changeset
|
52 |
val Error2 = """^(I found no .+)$""".r |
2f023b2b0e1e
more uniform bibtex error, without using perl (see 4710dd5093a3);
wenzelm
parents:
73565
diff
changeset
|
53 |
val Error3 = """^(.+)---line (\d+) of file (.+)""".r |
67203 | 54 |
Line.logical_lines(File.read(log_path)).flatMap(line => |
55 |
line match { |
|
67300 | 56 |
case Error1(msg) => Some("Bibtex error: " + msg) |
73730
2f023b2b0e1e
more uniform bibtex error, without using perl (see 4710dd5093a3);
wenzelm
parents:
73565
diff
changeset
|
57 |
case Error2(msg) => Some("Bibtex error: " + msg) |
2f023b2b0e1e
more uniform bibtex error, without using perl (see 4710dd5093a3);
wenzelm
parents:
73565
diff
changeset
|
58 |
case Error3(msg, Value.Int(l), file) => |
67203 | 59 |
val path = File.standard_path(file) |
60 |
if (Path.is_wellformed(path)) { |
|
61 |
val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode) |
|
62 |
Some("Bibtex error" + Position.here(pos) + ":\n " + msg) |
|
63 |
} |
|
64 |
else None |
|
65 |
case _ => None |
|
66 |
}) |
|
67 |
} |
|
68 |
else Nil |
|
69 |
} |
|
70 |
||
71 |
||
72 |
||
67272 | 73 |
/** check database **/ |
74 |
||
75393 | 75 |
def check_database(database: String): (List[(String, Position.T)], List[(String, Position.T)]) = { |
67275
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
76 |
val chunks = parse(Line.normalize(database)) |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
77 |
var chunk_pos = Map.empty[String, Position.T] |
67272 | 78 |
val tokens = new mutable.ListBuffer[(Token, Position.T)] |
79 |
var line = 1 |
|
80 |
var offset = 1 |
|
81 |
||
67276 | 82 |
def make_pos(length: Int): Position.T = |
83 |
Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line) |
|
67272 | 84 |
|
75393 | 85 |
def advance_pos(tok: Token): Unit = { |
67272 | 86 |
for (s <- Symbol.iterator(tok.source)) { |
87 |
if (Symbol.is_newline(s)) line += 1 |
|
88 |
offset += 1 |
|
89 |
} |
|
90 |
} |
|
91 |
||
92 |
def get_line_pos(l: Int): Position.T = |
|
93 |
if (0 < l && l <= tokens.length) tokens(l - 1)._2 else Position.none |
|
94 |
||
95 |
for (chunk <- chunks) { |
|
96 |
val name = chunk.name |
|
97 |
if (name != "" && !chunk_pos.isDefinedAt(name)) { |
|
67276 | 98 |
chunk_pos += (name -> make_pos(chunk.heading_length)) |
67272 | 99 |
} |
100 |
for (tok <- chunk.tokens) { |
|
67276 | 101 |
tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length)) |
67272 | 102 |
advance_pos(tok) |
103 |
} |
|
104 |
} |
|
105 |
||
75394 | 106 |
Isabelle_System.with_tmp_dir("bibtex") { tmp_dir => |
67272 | 107 |
File.write(tmp_dir + Path.explode("root.bib"), |
108 |
tokens.iterator.map(p => p._1.source).mkString("", "\n", "\n")) |
|
109 |
File.write(tmp_dir + Path.explode("root.aux"), |
|
110 |
"\\bibstyle{plain}\n\\bibdata{root}\n\\citation{*}") |
|
111 |
Isabelle_System.bash("\"$ISABELLE_BIBTEX\" root", cwd = tmp_dir.file) |
|
112 |
||
113 |
val Error = """^(.*)---line (\d+) of file root.bib$""".r |
|
114 |
val Warning = """^Warning--(.+)$""".r |
|
115 |
val Warning_Line = """--line (\d+) of file root.bib$""".r |
|
116 |
val Warning_in_Chunk = """^Warning--(.+) in (.+)$""".r |
|
117 |
||
118 |
val log_file = tmp_dir + Path.explode("root.blg") |
|
119 |
val lines = if (log_file.is_file) Line.logical_lines(File.read(log_file)) else Nil |
|
120 |
||
67301 | 121 |
val (errors, warnings) = |
69294 | 122 |
if (lines.isEmpty) (Nil, Nil) |
123 |
else { |
|
124 |
lines.zip(lines.tail ::: List("")).flatMap( |
|
125 |
{ |
|
126 |
case (Error(msg, Value.Int(l)), _) => |
|
127 |
Some((true, (msg, get_line_pos(l)))) |
|
128 |
case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) => |
|
129 |
Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name)))) |
|
130 |
case (Warning(msg), Warning_Line(Value.Int(l))) => |
|
131 |
Some((false, (Word.capitalize(msg), get_line_pos(l)))) |
|
132 |
case (Warning(msg), _) => |
|
133 |
Some((false, (Word.capitalize(msg), Position.none))) |
|
134 |
case _ => None |
|
135 |
} |
|
136 |
).partition(_._1) |
|
137 |
} |
|
67301 | 138 |
(errors.map(_._2), warnings.map(_._2)) |
75394 | 139 |
} |
67272 | 140 |
} |
141 |
||
75393 | 142 |
object Check_Database extends Scala.Fun_String("bibtex_check_database") { |
72756 | 143 |
val here = Scala_Project.here |
75393 | 144 |
def apply(database: String): String = { |
72193 | 145 |
import XML.Encode._ |
146 |
YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))( |
|
147 |
check_database(database))) |
|
148 |
} |
|
67275
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
149 |
} |
5e427586cb57
check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents:
67274
diff
changeset
|
150 |
|
67272 | 151 |
|
152 |
||
64828 | 153 |
/** document model **/ |
154 |
||
67290 | 155 |
/* entries */ |
64828 | 156 |
|
75393 | 157 |
def entries(text: String): List[Text.Info[String]] = { |
64831 | 158 |
val result = new mutable.ListBuffer[Text.Info[String]] |
64828 | 159 |
var offset = 0 |
160 |
for (chunk <- Bibtex.parse(text)) { |
|
64831 | 161 |
val end_offset = offset + chunk.source.length |
162 |
if (chunk.name != "" && !chunk.is_command) |
|
163 |
result += Text.Info(Text.Range(offset, end_offset), chunk.name) |
|
164 |
offset = end_offset |
|
64828 | 165 |
} |
166 |
result.toList |
|
167 |
} |
|
168 |
||
75393 | 169 |
def entries_iterator[A, B <: Document.Model]( |
170 |
models: Map[A, B] |
|
171 |
): Iterator[Text.Info[(String, B)]] = { |
|
66150 | 172 |
for { |
173 |
(_, model) <- models.iterator |
|
174 |
info <- model.bibtex_entries.iterator |
|
175 |
} yield info.map((_, model)) |
|
176 |
} |
|
177 |
||
64828 | 178 |
|
66152 | 179 |
/* completion */ |
180 |
||
181 |
def completion[A, B <: Document.Model]( |
|
75393 | 182 |
history: Completion.History, |
183 |
rendering: Rendering, |
|
184 |
caret: Text.Offset, |
|
185 |
models: Map[A, B] |
|
186 |
): Option[Completion.Result] = { |
|
66152 | 187 |
for { |
72729 | 188 |
Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption |
66152 | 189 |
name1 <- Completion.clean_name(name) |
190 |
||
72856 | 191 |
original <- rendering.get_text(r) |
66152 | 192 |
original1 <- Completion.clean_name(Library.perhaps_unquote(original)) |
193 |
||
194 |
entries = |
|
195 |
(for { |
|
196 |
Text.Info(_, (entry, _)) <- entries_iterator(models) |
|
197 |
if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1 |
|
198 |
} yield entry).toList |
|
199 |
if entries.nonEmpty |
|
200 |
||
201 |
items = |
|
202 |
entries.sorted.map({ |
|
203 |
case entry => |
|
204 |
val full_name = Long_Name.qualify(Markup.CITATION, entry) |
|
205 |
val description = List(entry, "(BibTeX entry)") |
|
206 |
val replacement = quote(entry) |
|
75659
9bd92ac9328f
more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
wenzelm
parents:
75420
diff
changeset
|
207 |
Completion.Item(r, original, full_name, description, replacement, 0, false) |
66152 | 208 |
}).sorted(history.ordering).take(rendering.options.int("completion_limit")) |
209 |
} yield Completion.Result(r, original, false, items) |
|
210 |
} |
|
211 |
||
212 |
||
64828 | 213 |
|
58523 | 214 |
/** content **/ |
215 |
||
58529 | 216 |
private val months = List( |
58523 | 217 |
"jan", |
218 |
"feb", |
|
219 |
"mar", |
|
220 |
"apr", |
|
221 |
"may", |
|
222 |
"jun", |
|
223 |
"jul", |
|
224 |
"aug", |
|
225 |
"sep", |
|
226 |
"oct", |
|
227 |
"nov", |
|
228 |
"dec") |
|
58529 | 229 |
def is_month(s: String): Boolean = months.contains(s.toLowerCase) |
58523 | 230 |
|
58529 | 231 |
private val commands = List("preamble", "string") |
232 |
def is_command(s: String): Boolean = commands.contains(s.toLowerCase) |
|
58523 | 233 |
|
58524 | 234 |
sealed case class Entry( |
58526 | 235 |
kind: String, |
58523 | 236 |
required: List[String], |
237 |
optional_crossref: List[String], |
|
75393 | 238 |
optional_other: List[String] |
239 |
) { |
|
70230 | 240 |
val optional_standard: List[String] = List("url", "doi", "ee") |
241 |
||
58533 | 242 |
def is_required(s: String): Boolean = required.contains(s.toLowerCase) |
58529 | 243 |
def is_optional(s: String): Boolean = |
70230 | 244 |
optional_crossref.contains(s.toLowerCase) || |
245 |
optional_other.contains(s.toLowerCase) || |
|
246 |
optional_standard.contains(s.toLowerCase) |
|
58529 | 247 |
|
70230 | 248 |
def fields: List[String] = |
249 |
required ::: optional_crossref ::: optional_other ::: optional_standard |
|
250 |
||
58524 | 251 |
def template: String = |
58526 | 252 |
"@" + kind + "{,\n" + fields.map(x => " " + x + " = {},\n").mkString + "}\n" |
58524 | 253 |
} |
58523 | 254 |
|
66150 | 255 |
val known_entries: List[Entry] = |
58524 | 256 |
List( |
257 |
Entry("Article", |
|
258 |
List("author", "title"), |
|
259 |
List("journal", "year"), |
|
260 |
List("volume", "number", "pages", "month", "note")), |
|
261 |
Entry("InProceedings", |
|
262 |
List("author", "title"), |
|
263 |
List("booktitle", "year"), |
|
264 |
List("editor", "volume", "number", "series", "pages", "month", "address", |
|
265 |
"organization", "publisher", "note")), |
|
266 |
Entry("InCollection", |
|
267 |
List("author", "title", "booktitle"), |
|
268 |
List("publisher", "year"), |
|
269 |
List("editor", "volume", "number", "series", "type", "chapter", "pages", |
|
270 |
"edition", "month", "address", "note")), |
|
271 |
Entry("InBook", |
|
272 |
List("author", "editor", "title", "chapter"), |
|
273 |
List("publisher", "year"), |
|
274 |
List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")), |
|
275 |
Entry("Proceedings", |
|
276 |
List("title", "year"), |
|
277 |
List(), |
|
278 |
List("booktitle", "editor", "volume", "number", "series", "address", "month", |
|
279 |
"organization", "publisher", "note")), |
|
280 |
Entry("Book", |
|
281 |
List("author", "editor", "title"), |
|
282 |
List("publisher", "year"), |
|
283 |
List("volume", "number", "series", "address", "edition", "month", "note")), |
|
284 |
Entry("Booklet", |
|
285 |
List("title"), |
|
286 |
List(), |
|
287 |
List("author", "howpublished", "address", "month", "year", "note")), |
|
288 |
Entry("PhdThesis", |
|
289 |
List("author", "title", "school", "year"), |
|
290 |
List(), |
|
291 |
List("type", "address", "month", "note")), |
|
292 |
Entry("MastersThesis", |
|
293 |
List("author", "title", "school", "year"), |
|
294 |
List(), |
|
295 |
List("type", "address", "month", "note")), |
|
296 |
Entry("TechReport", |
|
297 |
List("author", "title", "institution", "year"), |
|
298 |
List(), |
|
299 |
List("type", "number", "address", "month", "note")), |
|
300 |
Entry("Manual", |
|
301 |
List("title"), |
|
302 |
List(), |
|
303 |
List("author", "organization", "address", "edition", "month", "year", "note")), |
|
304 |
Entry("Unpublished", |
|
305 |
List("author", "title", "note"), |
|
306 |
List(), |
|
307 |
List("month", "year")), |
|
308 |
Entry("Misc", |
|
309 |
List(), |
|
310 |
List(), |
|
311 |
List("author", "title", "howpublished", "month", "year", "note"))) |
|
58523 | 312 |
|
58529 | 313 |
def get_entry(kind: String): Option[Entry] = |
66150 | 314 |
known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase) |
58529 | 315 |
|
58530 | 316 |
def is_entry(kind: String): Boolean = get_entry(kind).isDefined |
317 |
||
58523 | 318 |
|
319 |
||
320 |
/** tokens and chunks **/ |
|
321 |
||
75393 | 322 |
object Token { |
323 |
object Kind extends Enumeration { |
|
58529 | 324 |
val COMMAND = Value("command") |
325 |
val ENTRY = Value("entry") |
|
58523 | 326 |
val KEYWORD = Value("keyword") |
327 |
val NAT = Value("natural number") |
|
58529 | 328 |
val STRING = Value("string") |
58531 | 329 |
val NAME = Value("name") |
58523 | 330 |
val IDENT = Value("identifier") |
58535 | 331 |
val SPACE = Value("white space") |
332 |
val COMMENT = Value("ignored text") |
|
58523 | 333 |
val ERROR = Value("bad input") |
334 |
} |
|
335 |
} |
|
336 |
||
75393 | 337 |
sealed case class Token(kind: Token.Kind.Value, source: String) { |
58530 | 338 |
def is_kind: Boolean = |
339 |
kind == Token.Kind.COMMAND || |
|
340 |
kind == Token.Kind.ENTRY || |
|
341 |
kind == Token.Kind.IDENT |
|
58531 | 342 |
def is_name: Boolean = |
343 |
kind == Token.Kind.NAME || |
|
344 |
kind == Token.Kind.IDENT |
|
58535 | 345 |
def is_ignored: Boolean = |
346 |
kind == Token.Kind.SPACE || |
|
347 |
kind == Token.Kind.COMMENT |
|
67276 | 348 |
def is_malformed: Boolean = |
349 |
kind == Token.Kind.ERROR |
|
350 |
def is_open: Boolean = |
|
351 |
kind == Token.Kind.KEYWORD && (source == "{" || source == "(") |
|
58523 | 352 |
} |
353 |
||
75393 | 354 |
case class Chunk(kind: String, tokens: List[Token]) { |
58529 | 355 |
val source = tokens.map(_.source).mkString |
58526 | 356 |
|
58530 | 357 |
private val content: Option[List[Token]] = |
58523 | 358 |
tokens match { |
59319 | 359 |
case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty => |
58529 | 360 |
(body.init.filterNot(_.is_ignored), body.last) match { |
58530 | 361 |
case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}")) |
362 |
if tok.is_kind => Some(toks) |
|
363 |
||
364 |
case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")")) |
|
365 |
if tok.is_kind => Some(toks) |
|
366 |
||
58528 | 367 |
case _ => None |
58523 | 368 |
} |
58528 | 369 |
case _ => None |
58526 | 370 |
} |
371 |
||
372 |
def name: String = |
|
58530 | 373 |
content match { |
58531 | 374 |
case Some(tok :: _) if tok.is_name => tok.source |
58523 | 375 |
case _ => "" |
376 |
} |
|
58530 | 377 |
|
67276 | 378 |
def heading_length: Int = |
379 |
if (name == "") 1 |
|
73359 | 380 |
else { |
381 |
tokens.takeWhile(tok => !tok.is_open).foldLeft(0) { case (n, tok) => n + tok.source.length } |
|
382 |
} |
|
67276 | 383 |
|
58530 | 384 |
def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored) |
385 |
def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed) |
|
58543 | 386 |
def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined |
387 |
def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined |
|
58523 | 388 |
} |
389 |
||
390 |
||
391 |
||
392 |
/** parsing **/ |
|
393 |
||
394 |
// context of partial line-oriented scans |
|
395 |
abstract class Line_Context |
|
58589 | 396 |
case object Ignored extends Line_Context |
58590
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
397 |
case object At extends Line_Context |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
398 |
case class Item_Start(kind: String) extends Line_Context |
58591 | 399 |
case class Item_Open(kind: String, end: String) extends Line_Context |
400 |
case class Item(kind: String, end: String, delim: Delimited) extends Line_Context |
|
58590
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
401 |
|
58528 | 402 |
case class Delimited(quoted: Boolean, depth: Int) |
403 |
val Closed = Delimited(false, 0) |
|
58523 | 404 |
|
405 |
private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source) |
|
406 |
private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source) |
|
407 |
||
408 |
||
68224 | 409 |
// See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web |
58523 | 410 |
// module @<Scan for and process a \.{.bib} command or database entry@>. |
411 |
||
75393 | 412 |
object Parsers extends RegexParsers { |
58523 | 413 |
/* white space and comments */ |
414 |
||
415 |
override val whiteSpace = "".r |
|
416 |
||
58535 | 417 |
private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE) |
58590
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
418 |
private val spaces = rep(space) |
58523 | 419 |
|
58528 | 420 |
|
58535 | 421 |
/* ignored text */ |
58528 | 422 |
|
423 |
private val ignored: Parser[Chunk] = |
|
58609 | 424 |
rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ { |
58535 | 425 |
case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) } |
58523 | 426 |
|
58536
402a8e8107a7
more total chunk_line: recovery via ignored_line;
wenzelm
parents:
58535
diff
changeset
|
427 |
private def ignored_line: Parser[(Chunk, Line_Context)] = |
58589 | 428 |
ignored ^^ { case a => (a, Ignored) } |
58536
402a8e8107a7
more total chunk_line: recovery via ignored_line;
wenzelm
parents:
58535
diff
changeset
|
429 |
|
58523 | 430 |
|
431 |
/* delimited string: outermost "..." or {...} and body with balanced {...} */ |
|
432 |
||
58534 | 433 |
// see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces |
58523 | 434 |
private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] = |
75393 | 435 |
new Parser[(String, Delimited)] { |
73120
c3589f2dff31
more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents:
72957
diff
changeset
|
436 |
require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0, |
c3589f2dff31
more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents:
72957
diff
changeset
|
437 |
"bad delimiter depth") |
58523 | 438 |
|
75393 | 439 |
def apply(in: Input) = { |
58523 | 440 |
val start = in.offset |
441 |
val end = in.source.length |
|
442 |
||
443 |
var i = start |
|
444 |
var q = delim.quoted |
|
445 |
var d = delim.depth |
|
446 |
var finished = false |
|
447 |
while (!finished && i < end) { |
|
448 |
val c = in.source.charAt(i) |
|
58534 | 449 |
|
58523 | 450 |
if (c == '"' && d == 0) { i += 1; d = 1; q = true } |
58532 | 451 |
else if (c == '"' && d == 1 && q) { |
452 |
i += 1; d = 0; q = false; finished = true |
|
453 |
} |
|
58523 | 454 |
else if (c == '{') { i += 1; d += 1 } |
58534 | 455 |
else if (c == '}') { |
456 |
if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true } |
|
457 |
else {i = start; finished = true } |
|
58532 | 458 |
} |
58523 | 459 |
else if (d > 0) i += 1 |
460 |
else finished = true |
|
461 |
} |
|
462 |
if (i == start) Failure("bad input", in) |
|
58528 | 463 |
else { |
464 |
val s = in.source.subSequence(start, i).toString |
|
465 |
Success((s, Delimited(q, d)), in.drop(i - start)) |
|
466 |
} |
|
58523 | 467 |
} |
468 |
}.named("delimited_depth") |
|
469 |
||
58528 | 470 |
private def delimited: Parser[Token] = |
471 |
delimited_depth(Closed) ^? |
|
472 |
{ case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) } |
|
58523 | 473 |
|
58534 | 474 |
private def recover_delimited: Parser[Token] = |
58609 | 475 |
"""["{][^@]*""".r ^^ token(Token.Kind.ERROR) |
58534 | 476 |
|
58590
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
477 |
def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] = |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
478 |
delimited_depth(ctxt.delim) ^^ { case (s, delim1) => |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
479 |
(Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } | |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
480 |
recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) } |
58523 | 481 |
|
482 |
||
483 |
/* other tokens */ |
|
484 |
||
485 |
private val at = "@" ^^ keyword |
|
486 |
||
487 |
private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT) |
|
488 |
||
58591 | 489 |
private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME) |
490 |
||
58529 | 491 |
private val identifier = |
492 |
"""[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r |
|
493 |
||
494 |
private val ident = identifier ^^ token(Token.Kind.IDENT) |
|
58523 | 495 |
|
58528 | 496 |
val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space)) |
497 |
||
498 |
||
58591 | 499 |
/* body */ |
500 |
||
501 |
private val body = |
|
502 |
delimited | (recover_delimited | other_token) |
|
503 |
||
504 |
private def body_line(ctxt: Item) = |
|
505 |
if (ctxt.delim.depth > 0) |
|
506 |
delimited_line(ctxt) |
|
507 |
else |
|
508 |
delimited_line(ctxt) | |
|
509 |
other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } | |
|
510 |
ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) } |
|
511 |
||
512 |
||
58530 | 513 |
/* items: command or entry */ |
58528 | 514 |
|
58530 | 515 |
private val item_kind = |
58529 | 516 |
identifier ^^ { case a => |
517 |
val kind = |
|
518 |
if (is_command(a)) Token.Kind.COMMAND |
|
58530 | 519 |
else if (is_entry(a)) Token.Kind.ENTRY |
58529 | 520 |
else Token.Kind.IDENT |
521 |
Token(kind, a) |
|
522 |
} |
|
523 |
||
58591 | 524 |
private val item_begin = |
525 |
"{" ^^ { case a => ("}", keyword(a)) } | |
|
526 |
"(" ^^ { case a => (")", keyword(a)) } |
|
527 |
||
528 |
private def item_name(kind: String) = |
|
529 |
kind.toLowerCase match { |
|
530 |
case "preamble" => failure("") |
|
531 |
case "string" => identifier ^^ token(Token.Kind.NAME) |
|
532 |
case _ => name |
|
533 |
} |
|
534 |
||
58531 | 535 |
private val item_start = |
58590
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
536 |
at ~ spaces ~ item_kind ~ spaces ^^ |
58528 | 537 |
{ case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) } |
538 |
||
58530 | 539 |
private val item: Parser[Chunk] = |
58591 | 540 |
(item_start ~ item_begin ~ spaces) into |
541 |
{ case (kind, a) ~ ((end, b)) ~ c => |
|
542 |
opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ { |
|
543 |
case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } } |
|
58528 | 544 |
|
58530 | 545 |
private val recover_item: Parser[Chunk] = |
58609 | 546 |
at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) } |
58528 | 547 |
|
58591 | 548 |
|
549 |
/* chunks */ |
|
58523 | 550 |
|
58528 | 551 |
val chunk: Parser[Chunk] = ignored | (item | recover_item) |
58523 | 552 |
|
75393 | 553 |
def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] = { |
58530 | 554 |
ctxt match { |
58589 | 555 |
case Ignored => |
58538
299b82d12d53
proper treatment of @comment (amending 402a8e8107a7);
wenzelm
parents:
58536
diff
changeset
|
556 |
ignored_line | |
58590
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
557 |
at ^^ { case a => (Chunk("", List(a)), At) } |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
558 |
|
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
559 |
case At => |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
560 |
space ^^ { case a => (Chunk("", List(a)), ctxt) } | |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
561 |
item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } | |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
562 |
recover_item ^^ { case a => (a, Ignored) } | |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
563 |
ignored_line |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
564 |
|
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
565 |
case Item_Start(kind) => |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
566 |
space ^^ { case a => (Chunk(kind, List(a)), ctxt) } | |
58591 | 567 |
item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } | |
58596 | 568 |
recover_item ^^ { case a => (a, Ignored) } | |
58590
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
569 |
ignored_line |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
570 |
|
58591 | 571 |
case Item_Open(kind, end) => |
58590
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
572 |
space ^^ { case a => (Chunk(kind, List(a)), ctxt) } | |
58591 | 573 |
item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } | |
574 |
body_line(Item(kind, end, Closed)) | |
|
58590
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
575 |
ignored_line |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
576 |
|
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
577 |
case item_ctxt: Item => |
58591 | 578 |
body_line(item_ctxt) | |
58590
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
579 |
ignored_line |
472b9fbcc7f0
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents:
58589
diff
changeset
|
580 |
|
58530 | 581 |
case _ => failure("") |
582 |
} |
|
583 |
} |
|
58528 | 584 |
} |
58523 | 585 |
|
586 |
||
58528 | 587 |
/* parse */ |
58523 | 588 |
|
589 |
def parse(input: CharSequence): List[Chunk] = |
|
64824 | 590 |
Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match { |
58523 | 591 |
case Parsers.Success(result, _) => result |
58526 | 592 |
case _ => error("Unexpected failure to parse input:\n" + input.toString) |
58523 | 593 |
} |
58528 | 594 |
|
75393 | 595 |
def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) = { |
64824 | 596 |
var in: Reader[Char] = Scan.char_reader(input) |
58528 | 597 |
val chunks = new mutable.ListBuffer[Chunk] |
598 |
var ctxt = context |
|
599 |
while (!in.atEnd) { |
|
75420 | 600 |
val result = Parsers.parse(Parsers.chunk_line(ctxt), in) |
601 |
(result : @unchecked) match { |
|
60215 | 602 |
case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest |
58528 | 603 |
case Parsers.NoSuccess(_, rest) => |
604 |
error("Unepected failure to parse input:\n" + rest.source.toString) |
|
605 |
} |
|
606 |
} |
|
607 |
(chunks.toList, ctxt) |
|
608 |
} |
|
67243 | 609 |
|
610 |
||
611 |
||
612 |
/** HTML output **/ |
|
613 |
||
614 |
private val output_styles = |
|
615 |
List( |
|
67257 | 616 |
"" -> "html-n", |
67243 | 617 |
"plain" -> "html-n", |
618 |
"alpha" -> "html-a", |
|
619 |
"named" -> "html-n", |
|
620 |
"paragraph" -> "html-n", |
|
621 |
"unsort" -> "html-u", |
|
622 |
"unsortlist" -> "html-u") |
|
623 |
||
624 |
def html_output(bib: List[Path], |
|
67256 | 625 |
title: String = "Bibliography", |
67248
68177abb2988
isabelle.preview presents bibtex database files as well;
wenzelm
parents:
67243
diff
changeset
|
626 |
body: Boolean = false, |
67243 | 627 |
citations: List[String] = List("*"), |
67257 | 628 |
style: String = "", |
75393 | 629 |
chronological: Boolean = false |
630 |
): String = { |
|
75394 | 631 |
Isabelle_System.with_tmp_dir("bibtex") { tmp_dir => |
67243 | 632 |
/* database files */ |
633 |
||
69367 | 634 |
val bib_files = bib.map(_.drop_ext) |
75393 | 635 |
val bib_names = { |
69366 | 636 |
val names0 = bib_files.map(_.file_name) |
67243 | 637 |
if (Library.duplicates(names0).isEmpty) names0 |
638 |
else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name }) |
|
639 |
} |
|
640 |
||
641 |
for ((a, b) <- bib_files zip bib_names) { |
|
73317 | 642 |
Isabelle_System.copy_file(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib")) |
67243 | 643 |
} |
644 |
||
645 |
||
646 |
/* style file */ |
|
647 |
||
648 |
val bst = |
|
649 |
output_styles.toMap.get(style) match { |
|
650 |
case Some(base) => base + (if (chronological) "c" else "") + ".bst" |
|
651 |
case None => |
|
652 |
error("Bad style for bibtex HTML output: " + quote(style) + |
|
653 |
"\n(expected: " + commas_quote(output_styles.map(_._1)) + ")") |
|
654 |
} |
|
73317 | 655 |
Isabelle_System.copy_file(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir) |
67243 | 656 |
|
657 |
||
658 |
/* result */ |
|
659 |
||
660 |
val in_file = Path.explode("bib.aux") |
|
661 |
val out_file = Path.explode("bib.html") |
|
662 |
||
663 |
File.write(tmp_dir + in_file, |
|
664 |
bib_names.mkString("\\bibdata{", ",", "}\n") + |
|
665 |
citations.map(cite => "\\citation{" + cite + "}\n").mkString) |
|
666 |
||
667 |
Isabelle_System.bash( |
|
668 |
"\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" + |
|
67257 | 669 |
" -u -s " + Bash.string(proper_string(style) getOrElse "empty") + |
670 |
(if (chronological) " -c" else "") + |
|
67256 | 671 |
(if (title != "") " -h " + Bash.string(title) + " " else "") + |
672 |
" " + File.bash_path(in_file) + " " + File.bash_path(out_file), |
|
67243 | 673 |
cwd = tmp_dir.file).check |
674 |
||
675 |
val html = File.read(tmp_dir + out_file) |
|
676 |
||
67248
68177abb2988
isabelle.preview presents bibtex database files as well;
wenzelm
parents:
67243
diff
changeset
|
677 |
if (body) { |
68177abb2988
isabelle.preview presents bibtex database files as well;
wenzelm
parents:
67243
diff
changeset
|
678 |
cat_lines( |
68177abb2988
isabelle.preview presents bibtex database files as well;
wenzelm
parents:
67243
diff
changeset
|
679 |
split_lines(html). |
68177abb2988
isabelle.preview presents bibtex database files as well;
wenzelm
parents:
67243
diff
changeset
|
680 |
dropWhile(line => !line.startsWith("<!-- BEGIN BIBLIOGRAPHY")).reverse. |
68177abb2988
isabelle.preview presents bibtex database files as well;
wenzelm
parents:
67243
diff
changeset
|
681 |
dropWhile(line => !line.startsWith("<!-- END BIBLIOGRAPHY")).reverse) |
68177abb2988
isabelle.preview presents bibtex database files as well;
wenzelm
parents:
67243
diff
changeset
|
682 |
} |
68177abb2988
isabelle.preview presents bibtex database files as well;
wenzelm
parents:
67243
diff
changeset
|
683 |
else html |
75394 | 684 |
} |
67243 | 685 |
} |
58523 | 686 |
} |