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