1/* Title: Pure/Thy/html.scala 2 Author: Makarius 3 4HTML presentation elements. 5*/ 6 7package isabelle 8 9 10object HTML 11{ 12 /* output text with control symbols */ 13 14 private val control = 15 Map( 16 Symbol.sub -> "sub", Symbol.sub_decoded -> "sub", 17 Symbol.sup -> "sup", Symbol.sup_decoded -> "sup", 18 Symbol.bold -> "b", Symbol.bold_decoded -> "b") 19 20 private val control_block = 21 Map( 22 Symbol.bsub -> "<sub>", Symbol.bsub_decoded -> "<sub>", 23 Symbol.esub -> "</sub>", Symbol.esub_decoded -> "</sub>", 24 Symbol.bsup -> "<sup>", Symbol.bsup_decoded -> "<sup>", 25 Symbol.esup -> "</sup>", Symbol.esup_decoded -> "</sup>") 26 27 def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym) 28 29 def output_char_permissive(c: Char, s: StringBuilder) 30 { 31 c match { 32 case '<' => s ++= "<" 33 case '>' => s ++= ">" 34 case '&' => s ++= "&" 35 case _ => s += c 36 } 37 } 38 39 def output(text: String, s: StringBuilder, hidden: Boolean, permissive: Boolean) 40 { 41 def output_char(c: Char): Unit = 42 if (permissive) output_char_permissive(c, s) 43 else XML.output_char(c, s) 44 45 def output_string(str: String): Unit = 46 str.iterator.foreach(output_char) 47 48 def output_hidden(body: => Unit): Unit = 49 if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" } 50 51 def output_symbol(sym: Symbol.Symbol): Unit = 52 if (sym != "") { 53 control_block.get(sym) match { 54 case Some(html) if html.startsWith("</") => 55 s ++= html; output_hidden(output_string(sym)) 56 case Some(html) => 57 output_hidden(output_string(sym)); s ++= html 58 case None => 59 if (hidden && Symbol.is_control_encoded(sym)) { 60 output_hidden(output_string(Symbol.control_prefix)) 61 s ++= "<span class=\"control\">" 62 output_string(Symbol.control_name(sym).get) 63 s ++= "</span>" 64 output_hidden(output_string(Symbol.control_suffix)) 65 } 66 else output_string(sym) 67 } 68 } 69 70 var ctrl = "" 71 for (sym <- Symbol.iterator(text)) { 72 if (is_control(sym)) { output_symbol(ctrl); ctrl = sym } 73 else { 74 control.get(ctrl) match { 75 case Some(elem) if Symbol.is_controllable(sym) => 76 output_hidden(output_symbol(ctrl)) 77 s += '<'; s ++= elem; s += '>' 78 output_symbol(sym) 79 s ++= "</"; s ++= elem; s += '>' 80 case _ => 81 output_symbol(ctrl) 82 output_symbol(sym) 83 } 84 ctrl = "" 85 } 86 } 87 output_symbol(ctrl) 88 } 89 90 def output(text: String): String = 91 Library.make_string(output(text, _, hidden = false, permissive = true)) 92 93 94 /* output XML as HTML */ 95 96 private val structural_elements = 97 Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6", 98 "ul", "ol", "dl", "li", "dt", "dd") 99 100 def output(body: XML.Body, s: StringBuilder, hidden: Boolean, structural: Boolean) 101 { 102 def elem(markup: Markup) 103 { 104 s ++= markup.name 105 for ((a, b) <- markup.properties) { 106 s += ' ' 107 s ++= a 108 s += '=' 109 s += '"' 110 output(b, s, hidden = hidden, permissive = false) 111 s += '"' 112 } 113 } 114 def tree(t: XML.Tree): Unit = 115 t match { 116 case XML.Elem(markup, Nil) => 117 s += '<'; elem(markup); s ++= "/>" 118 case XML.Elem(markup, ts) => 119 if (structural && structural_elements(markup.name)) s += '\n' 120 s += '<'; elem(markup); s += '>' 121 ts.foreach(tree) 122 s ++= "</"; s ++= markup.name; s += '>' 123 if (structural && structural_elements(markup.name)) s += '\n' 124 case XML.Text(txt) => 125 output(txt, s, hidden = hidden, permissive = true) 126 } 127 body.foreach(tree) 128 } 129 130 def output(body: XML.Body, hidden: Boolean, structural: Boolean): String = 131 Library.make_string(output(body, _, hidden, structural)) 132 133 def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String = 134 output(List(tree), hidden, structural) 135 136 137 /* attributes */ 138 139 class Attribute(val name: String, value: String) 140 { 141 def xml: XML.Attribute = name -> value 142 def apply(elem: XML.Elem): XML.Elem = elem + xml 143 } 144 145 def id(s: String): Attribute = new Attribute("id", s) 146 def class_(name: String): Attribute = new Attribute("class", name) 147 148 def width(w: Int): Attribute = new Attribute("width", w.toString) 149 def height(h: Int): Attribute = new Attribute("height", h.toString) 150 def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem)) 151 152 153 /* structured markup operators */ 154 155 def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt)) 156 val no_text: XML.Tree = XML.Text("") 157 val break: XML.Body = List(XML.elem("br")) 158 159 class Operator(val name: String) 160 { 161 def apply(body: XML.Body): XML.Elem = XML.elem(name, body) 162 def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body)) 163 def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body) 164 } 165 166 class Heading(name: String) extends Operator(name) 167 { 168 def apply(txt: String): XML.Elem = super.apply(text(txt)) 169 def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt)) 170 def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt)) 171 } 172 173 val div = new Operator("div") 174 val span = new Operator("span") 175 val pre = new Operator("pre") 176 val par = new Operator("p") 177 val emph = new Operator("em") 178 val bold = new Operator("b") 179 val code = new Operator("code") 180 val item = new Operator("li") 181 val list = new Operator("ul") 182 val enum = new Operator("ol") 183 val descr = new Operator("dl") 184 val dt = new Operator("dt") 185 val dd = new Operator("dd") 186 187 val title = new Heading("title") 188 val chapter = new Heading("h1") 189 val section = new Heading("h2") 190 val subsection = new Heading("h3") 191 val subsubsection = new Heading("h4") 192 val paragraph = new Heading("h5") 193 val subparagraph = new Heading("h6") 194 195 def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_))) 196 def enumerate(items: List[XML.Body]): XML.Elem = enum(items.map(item(_))) 197 def description(items: List[(XML.Body, XML.Body)]): XML.Elem = 198 descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) })) 199 200 def link(href: String, body: XML.Body = Nil): XML.Elem = 201 XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body) 202 203 def image(src: String, alt: String = ""): XML.Elem = 204 XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) 205 206 def source(body: XML.Body): XML.Elem = pre("source", body) 207 def source(src: String): XML.Elem = source(text(src)) 208 209 def style(s: String): XML.Elem = XML.elem("style", text(s)) 210 def style_file(href: String): XML.Elem = 211 XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil) 212 def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file)) 213 214 def script(s: String): XML.Elem = XML.elem("script", text(s)) 215 def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil) 216 def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file)) 217 218 219 /* messages */ 220 221 // background 222 val writeln_message: Attribute = class_("writeln_message") 223 val warning_message: Attribute = class_("warning_message") 224 val error_message: Attribute = class_("error_message") 225 226 // underline 227 val writeln: Attribute = class_("writeln") 228 val warning: Attribute = class_("warning") 229 val error: Attribute = class_("error") 230 231 232 /* tooltips */ 233 234 def tooltip(item: XML.Body, tip: XML.Body): XML.Elem = 235 span(item ::: List(div("tooltip", tip))) 236 237 def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem = 238 HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg))))) 239 240 241 /* GUI elements */ 242 243 object GUI 244 { 245 private def optional_value(text: String): XML.Attributes = 246 proper_string(text).map(a => "value" -> a).toList 247 248 private def optional_name(name: String): XML.Attributes = 249 proper_string(name).map(a => "name" -> a).toList 250 251 private def optional_title(tooltip: String): XML.Attributes = 252 proper_string(tooltip).map(a => "title" -> a).toList 253 254 private def optional_submit(submit: Boolean): XML.Attributes = 255 if (submit) List("onChange" -> "this.form.submit()") else Nil 256 257 private def optional_checked(selected: Boolean): XML.Attributes = 258 if (selected) List("checked" -> "") else Nil 259 260 private def optional_action(action: String): XML.Attributes = 261 proper_string(action).map(a => "action" -> a).toList 262 263 private def optional_onclick(script: String): XML.Attributes = 264 proper_string(script).map(a => "onclick" -> a).toList 265 266 private def optional_onchange(script: String): XML.Attributes = 267 proper_string(script).map(a => "onchange" -> a).toList 268 269 def button(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false, 270 script: String = ""): XML.Elem = 271 XML.Elem( 272 Markup("button", 273 List("type" -> (if (submit) "submit" else "button"), "value" -> "true") ::: 274 optional_name(name) ::: optional_title(tooltip) ::: optional_onclick(script)), body) 275 276 def checkbox(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false, 277 selected: Boolean = false, script: String = ""): XML.Elem = 278 XML.elem("label", 279 XML.elem( 280 Markup("input", 281 List("type" -> "checkbox", "value" -> "true") ::: optional_name(name) ::: 282 optional_title(tooltip) ::: optional_submit(submit) ::: 283 optional_checked(selected) ::: optional_onchange(script))) :: body) 284 285 def text_field(columns: Int = 0, text: String = "", name: String = "", tooltip: String = "", 286 submit: Boolean = false, script: String = ""): XML.Elem = 287 XML.elem(Markup("input", 288 List("type" -> "text") ::: 289 (if (columns > 0) List("size" -> columns.toString) else Nil) ::: 290 optional_value(text) ::: optional_name(name) ::: optional_title(tooltip) ::: 291 optional_submit(submit) ::: optional_onchange(script))) 292 293 def parameter(text: String = "", name: String = ""): XML.Elem = 294 XML.elem( 295 Markup("input", List("type" -> "hidden") ::: optional_value(text) ::: optional_name(name))) 296 297 def form(body: XML.Body, name: String = "", action: String = "", http_post: Boolean = false) 298 : XML.Elem = 299 XML.Elem( 300 Markup("form", optional_name(name) ::: optional_action(action) ::: 301 (if (http_post) List("method" -> "post") else Nil)), body) 302 } 303 304 305 /* GUI layout */ 306 307 object Wrap_Panel 308 { 309 object Alignment extends Enumeration 310 { 311 val left, right, center = Value 312 } 313 314 def apply(contents: List[XML.Elem], name: String = "", action: String = "", 315 alignment: Alignment.Value = Alignment.right): XML.Elem = 316 { 317 val body = Library.separate(XML.Text(" "), contents) 318 GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))), 319 name = name, action = action) 320 } 321 } 322 323 324 /* document */ 325 326 val header: String = 327 XML.header + 328 """<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> 329<html xmlns="http://www.w3.org/1999/xhtml">""" 330 331 val head_meta: XML.Elem = 332 XML.Elem(Markup("meta", 333 List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) 334 335 def output_document(head: XML.Body, body: XML.Body, 336 css: String = "isabelle.css", 337 hidden: Boolean = true, 338 structural: Boolean = true): String = 339 { 340 cat_lines( 341 List(header, 342 output( 343 XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head), 344 hidden = hidden, structural = structural), 345 output(XML.elem("body", body), 346 hidden = hidden, structural = structural))) 347 } 348 349 350 /* fonts */ 351 352 def fonts_url(): String => String = 353 (for (entry <- Isabelle_Fonts.fonts(hidden = true)) 354 yield (entry.path.file_name -> Url.print_file(entry.path.file))).toMap 355 356 def fonts_dir(prefix: String)(ttf_name: String): String = 357 prefix + "/" + ttf_name 358 359 def fonts_css(make_url: String => String = fonts_url()): String = 360 { 361 def font_face(entry: Isabelle_Fonts.Entry): String = 362 cat_lines( 363 List( 364 "@font-face {", 365 " font-family: '" + entry.family + "';", 366 " src: url('" + make_url(entry.path.file_name) + "') format('truetype');") ::: 367 (if (entry.is_bold) List(" font-weight: bold;") else Nil) ::: 368 (if (entry.is_italic) List(" font-style: italic;") else Nil) ::: 369 List("}")) 370 371 ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face(_))) 372 .mkString("", "\n\n", "\n") 373 } 374 375 376 /* document directory */ 377 378 def isabelle_css: Path = Path.explode("~~/etc/isabelle.css") 379 380 def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts")) 381 { 382 File.write(dir + isabelle_css.base, 383 fonts_css(make_url) + "\n\n" + File.read(isabelle_css)) 384 } 385 386 def init_dir(dir: Path) 387 { 388 Isabelle_System.mkdirs(dir) 389 write_isabelle_css(dir) 390 } 391 392 def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body, 393 css: String = isabelle_css.file_name, 394 hidden: Boolean = true, 395 structural: Boolean = true) 396 { 397 init_dir(dir) 398 File.write(dir + Path.basic(name), 399 output_document(head, body, css = css, hidden = hidden, structural = structural)) 400 } 401} 402