src/Pure/Thy/present.scala
changeset 67256 ce7d856680d1
parent 67253 93b4333f33bb
child 67260 ecd607631bc7
equal deleted inserted replaced
67255:f1f983484878 67256:ce7d856680d1
   106   def preview(fonts_dir: String, snapshot: Document.Snapshot, plain: Boolean = false): String =
   106   def preview(fonts_dir: String, snapshot: Document.Snapshot, plain: Boolean = false): String =
   107   {
   107   {
   108     require(!snapshot.is_outdated)
   108     require(!snapshot.is_outdated)
   109 
   109 
   110     val name = snapshot.node_name
   110     val name = snapshot.node_name
   111     if (name.is_bibtex && !plain) Bibtex.present(snapshot)
   111     if (name.is_bibtex && !plain) {
       
   112       val title = "Bibliography " + quote(name.path.base_name)
       
   113       Isabelle_System.with_tmp_file("bib", "bib") { bib =>
       
   114         File.write(bib, snapshot.node.source)
       
   115         Bibtex.html_output(List(bib), style = "unsort", title = title)
       
   116       }
       
   117     }
   112     else {
   118     else {
   113       val (heading, body) =
   119       val (title, body) =
   114         if (name.is_theory && !plain)
   120         if (name.is_theory && !plain)
   115           ("Theory " + quote(name.theory_base_name), pide_document(snapshot))
   121           ("Theory " + quote(name.theory_base_name), pide_document(snapshot))
   116         else ("File " + quote(name.path.base_name), text_document(snapshot))
   122         else ("File " + quote(name.path.base_name), text_document(snapshot))
   117 
   123 
   118       HTML.output_document(
   124       HTML.output_document(
   119         List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css)),
   125         List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css)),
   120           HTML.title(heading)),
   126           HTML.title(title)),
   121           List(HTML.chapter(heading), HTML.source(body)))
   127           List(HTML.chapter(title), HTML.source(body)))
   122     }
   128     }
   123   }
   129   }
   124 
   130 
   125 
   131 
   126   /* theory document */
   132   /* theory document */