1/* Title: Pure/Thy/present.scala 2 Author: Makarius 3 4Theory presentation: HTML. 5*/ 6 7package isabelle 8 9 10import java.io.{File => JFile} 11 12import scala.collection.immutable.SortedMap 13 14 15object Present 16{ 17 /* maintain chapter index -- NOT thread-safe */ 18 19 private val sessions_path = Path.basic(".sessions") 20 21 private def read_sessions(dir: Path): List[(String, String)] = 22 { 23 val path = dir + sessions_path 24 if (path.is_file) { 25 import XML.Decode._ 26 list(pair(string, string))(Symbol.decode_yxml(File.read(path))) 27 } 28 else Nil 29 } 30 31 private def write_sessions(dir: Path, sessions: List[(String, String)]) 32 { 33 import XML.Encode._ 34 File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) 35 } 36 37 def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)]) 38 { 39 val dir = browser_info + Path.basic(chapter) 40 Isabelle_System.mkdirs(dir) 41 42 val sessions0 = 43 try { read_sessions(dir) } 44 catch { case _: XML.Error => Nil } 45 46 val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList 47 write_sessions(dir, sessions) 48 49 val title = "Isabelle/" + chapter + " sessions" 50 HTML.write_document(dir, "index.html", 51 List(HTML.title(title + " (" + Distribution.version + ")")), 52 HTML.chapter(title) :: 53 (if (sessions.isEmpty) Nil 54 else 55 List(HTML.div("sessions", 56 List(HTML.description( 57 sessions.map({ case (name, description) => 58 (List(HTML.link(name + "/index.html", HTML.text(name))), 59 if (description == "") Nil 60 else HTML.break ::: List(HTML.pre(HTML.text(description)))) }))))))) 61 } 62 63 def make_global_index(browser_info: Path) 64 { 65 if (!(browser_info + Path.explode("index.html")).is_file) { 66 Isabelle_System.mkdirs(browser_info) 67 File.copy(Path.explode("~~/lib/logo/isabelle.gif"), 68 browser_info + Path.explode("isabelle.gif")) 69 File.write(browser_info + Path.explode("index.html"), 70 File.read(Path.explode("~~/lib/html/library_index_header.template")) + 71 File.read(Path.explode("~~/lib/html/library_index_content.template")) + 72 File.read(Path.explode("~~/lib/html/library_index_footer.template"))) 73 } 74 } 75 76 77 /* finish session */ 78 79 def finish( 80 progress: Progress, 81 browser_info: Path, 82 graph_file: JFile, 83 info: Sessions.Info, 84 name: String) 85 { 86 val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name) 87 val session_fonts = session_prefix + Path.explode("fonts") 88 89 if (info.options.bool("browser_info")) { 90 Isabelle_System.mkdirs(session_fonts) 91 92 val session_graph = session_prefix + Path.basic("session_graph.pdf") 93 File.copy(graph_file, session_graph.file) 94 Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph)) 95 96 HTML.write_isabelle_css(session_prefix) 97 98 for (font <- Isabelle_System.fonts(html = true)) 99 File.copy(font, session_fonts) 100 } 101 } 102 103 104 /** preview **/ 105 106 sealed case class Preview(title: String, content: String) 107 108 def preview(snapshot: Document.Snapshot, 109 plain_text: Boolean = false, 110 fonts_url: String => String = HTML.fonts_url()): Preview = 111 { 112 require(!snapshot.is_outdated) 113 114 def output_document(title: String, body: XML.Body): String = 115 HTML.output_document( 116 List( 117 HTML.style(HTML.fonts_css(fonts_url) + File.read(HTML.isabelle_css)), 118 HTML.title(title)), 119 List(HTML.source(body)), css = "", structural = false) 120 121 val name = snapshot.node_name 122 if (plain_text) { 123 val title = "File " + quote(name.path.base_name) 124 val content = output_document(title, HTML.text(snapshot.node.source)) 125 Preview(title, content) 126 } 127 else if (name.is_bibtex) { 128 val title = "Bibliography " + quote(name.path.base_name) 129 val content = 130 Isabelle_System.with_tmp_file("bib", "bib") { bib => 131 File.write(bib, snapshot.node.source) 132 Bibtex.html_output(List(bib), style = "unsort", title = title) 133 } 134 Preview(title, content) 135 } 136 else { 137 val title = 138 if (name.is_theory) "Theory " + quote(name.theory_base_name) 139 else "File " + quote(name.path.base_name) 140 val content = output_document(title, pide_document(snapshot)) 141 Preview(title, content) 142 } 143 } 144 145 146 /* PIDE document */ 147 148 private val document_elements = 149 Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements + 150 Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE 151 152 private val div_elements = 153 Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, 154 HTML.descr.name) 155 156 private def html_div(html: XML.Body): Boolean = 157 html exists { 158 case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body) 159 case XML.Text(_) => false 160 } 161 162 private def html_class(c: String, html: XML.Body): XML.Tree = 163 if (html.forall(_ == HTML.no_text)) HTML.no_text 164 else if (html_div(html)) HTML.div(c, html) 165 else HTML.span(c, html) 166 167 private def make_html(xml: XML.Body): XML.Body = 168 xml map { 169 case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) => 170 html_class(Markup.Language.DOCUMENT, make_html(body)) 171 case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body)) 172 case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body)) 173 case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text 174 case XML.Elem(Markup.Markdown_List(kind), body) => 175 if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body)) 176 case XML.Elem(markup, body) => 177 val name = markup.name 178 val html = 179 markup.properties match { 180 case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => 181 List(html_class(kind, make_html(body))) 182 case _ => 183 make_html(body) 184 } 185 Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { 186 case Some(c) => html_class(c.toString, html) 187 case None => html_class(name, html) 188 } 189 case XML.Text(text) => 190 XML.Text(Symbol.decode(text)) 191 } 192 193 def pide_document(snapshot: Document.Snapshot): XML.Body = 194 make_html(snapshot.markup_to_XML(Text.Range.full, document_elements)) 195 196 197 198 /** build document **/ 199 200 val default_document_name = "document" 201 val default_document_format = "pdf" 202 val document_formats = List("pdf", "dvi") 203 def default_document_dir(name: String): Path = Path.explode("output") + Path.basic(name) 204 205 def document_tags(tags: List[String]): String = 206 { 207 cat_lines( 208 tags.map(tag => 209 tag.toList match { 210 case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" 211 case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" 212 case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" 213 case cs => "\\isakeeptag{" + cs.mkString + "}" 214 })) + "\n" 215 } 216 217 def build_document( 218 document_name: String = default_document_name, 219 document_format: String = default_document_format, 220 document_dir: Option[Path] = None, 221 tags: List[String] = Nil) 222 { 223 val document_target = Path.parent + Path.explode(document_name).ext(document_format) 224 225 if (!document_formats.contains(document_format)) 226 error("Bad document output format: " + quote(document_format)) 227 228 val dir = document_dir getOrElse default_document_dir(document_name) 229 if (!dir.is_dir) error("Bad document output directory " + dir) 230 231 val root_name = 232 { 233 val root1 = "root_" + document_name 234 if ((dir + Path.explode(root1).ext("tex")).is_file) root1 else "root" 235 } 236 237 238 /* bash scripts */ 239 240 def root_bash(ext: String): String = Bash.string(root_name + "." + ext) 241 242 def latex_bash(fmt: String, ext: String = "tex"): String = 243 "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root_name + "." + ext) 244 245 def bash(script: String): Process_Result = 246 Isabelle_System.bash(script, cwd = dir.file) 247 248 249 /* prepare document */ 250 251 File.write(dir + Path.explode("isabelletags.sty"), document_tags(tags)) 252 253 List("log", "blg").foreach(ext => (dir + Path.explode(root_name).ext(ext)).file.delete) 254 255 val result = 256 if ((dir + Path.explode("build")).is_file) { 257 bash("./build " + Bash.string(document_format) + " " + Bash.string(document_name)) 258 } 259 else { 260 bash( 261 List( 262 latex_bash("sty"), 263 latex_bash(document_format), 264 "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }", 265 "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }", 266 latex_bash(document_format), 267 latex_bash(document_format)).mkString(" && ")) 268 } 269 270 271 /* result */ 272 273 if (!result.ok) { 274 cat_error( 275 Library.trim_line(result.err), 276 cat_lines(Latex.latex_errors(dir, root_name) ::: Bibtex.bibtex_errors(dir, root_name)), 277 "Failed to build document in " + File.path(dir.absolute_file)) 278 } 279 280 bash("if [ -f " + root_bash(document_format) + " ]; then cp -f " + 281 root_bash(document_format) + " " + File.bash_path(document_target) + "; fi").check 282 } 283 284 285 /* Isabelle tool wrapper */ 286 287 val isabelle_tool = 288 Isabelle_Tool("document", "prepare theory session document", args => 289 { 290 var document_dir: Option[Path] = None 291 var document_name = default_document_name 292 var document_format = default_document_format 293 var tags: List[String] = Nil 294 295 val getopts = Getopts(""" 296Usage: isabelle document [OPTIONS] 297 298 Options are: 299 -d DIR document output directory (default """ + 300 default_document_dir(default_document_name) + """) 301 -n NAME document name (default """ + quote(default_document_name) + """) 302 -o FORMAT document format: """ + 303 commas(document_formats.map(fmt => 304 fmt + (if (fmt == default_document_format) " (default)" else ""))) + """ 305 -t TAGS markup for tagged regions 306 307 Prepare the theory session document in document directory, producing the 308 specified output format. 309""", 310 "d:" -> (arg => document_dir = Some(Path.explode(arg))), 311 "n:" -> (arg => document_name = arg), 312 "o:" -> (arg => document_format = arg), 313 "t:" -> (arg => tags = space_explode(',', arg))) 314 315 val more_args = getopts(args) 316 if (more_args.nonEmpty) getopts.usage() 317 318 try { 319 build_document(document_dir = document_dir, document_name = document_name, 320 document_format = document_format, tags = tags) 321 } 322 catch { case ERROR(msg) => Output.writeln(msg); sys.exit(1) } 323 }) 324} 325