src/Pure/Thy/bibtex.scala
changeset 69366 b6dacf6eabe3
parent 69294 085f31ae902d
child 69367 34b7550b66c7
equal deleted inserted replaced
69365:c5b3860d29ef 69366:b6dacf6eabe3
    31 
    31 
    32     override def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
    32     override def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
    33     {
    33     {
    34       val name = snapshot.node_name
    34       val name = snapshot.node_name
    35       if (detect(name.node)) {
    35       if (detect(name.node)) {
    36         val title = "Bibliography " + quote(snapshot.node_name.path.base_name)
    36         val title = "Bibliography " + quote(snapshot.node_name.path.file_name)
    37         val content =
    37         val content =
    38           Isabelle_System.with_tmp_file("bib", "bib") { bib =>
    38           Isabelle_System.with_tmp_file("bib", "bib") { bib =>
    39             File.write(bib, snapshot.node.source)
    39             File.write(bib, snapshot.node.source)
    40             Bibtex.html_output(List(bib), style = "unsort", title = title)
    40             Bibtex.html_output(List(bib), style = "unsort", title = title)
    41           }
    41           }
   635       /* database files */
   635       /* database files */
   636 
   636 
   637       val bib_files = bib.map(path => path.split_ext._1)
   637       val bib_files = bib.map(path => path.split_ext._1)
   638       val bib_names =
   638       val bib_names =
   639       {
   639       {
   640         val names0 = bib_files.map(_.base_name)
   640         val names0 = bib_files.map(_.file_name)
   641         if (Library.duplicates(names0).isEmpty) names0
   641         if (Library.duplicates(names0).isEmpty) names0
   642         else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name })
   642         else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name })
   643       }
   643       }
   644 
   644 
   645       for ((a, b) <- bib_files zip bib_names) {
   645       for ((a, b) <- bib_files zip bib_names) {