# HG changeset patch # User wenzelm # Date 1496259470 -7200 # Node ID 8040d2563593004f17e5d2d5f067a65aefd608df # Parent 44e44bfc738a98b7dd527ebeedeee99e92fbbd67 modernized generated HTML; diff -r 44e44bfc738a -r 8040d2563593 etc/isabelle.css --- a/etc/isabelle.css Wed May 31 20:43:59 2017 +0200 +++ b/etc/isabelle.css Wed May 31 21:37:50 2017 +0200 @@ -40,6 +40,8 @@ .theories { background-color: #FFFFFF; padding: 10px; } .sessions { background-color: #FFFFFF; padding: 10px; } +.sessions pre { margin: 0px; } + .name { font-style: italic; } .filename { font-family: fixed; } diff -r 44e44bfc738a -r 8040d2563593 src/Pure/Admin/news.scala --- a/src/Pure/Admin/news.scala Wed May 31 20:43:59 2017 +0200 +++ b/src/Pure/Admin/news.scala Wed May 31 21:37:50 2017 +0200 @@ -17,18 +17,14 @@ val target_fonts = target + Path.explode("fonts") Isabelle_System.mkdirs(target_fonts) - File.write(target + Path.explode("NEWS.html"), - HTML.begin_document("NEWS") + - "\n
" + - HTML.output(Symbol.decode(File.read(Path.explode("~~/NEWS")))) + - "\n" + - HTML.end_document) - - for (font <- Isabelle_System.fonts(html = true)) File.copy(font, target_fonts) - File.copy(Path.explode("~~/etc/isabelle.css"), target) + HTML.write_document(target, "NEWS.html", + List(HTML.title("NEWS (" + Distribution.version + ")")), + List( + HTML.chapter("NEWS"), + HTML.source(Symbol.decode(File.read(Path.explode("~~/NEWS")))))) } diff -r 44e44bfc738a -r 8040d2563593 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Wed May 31 20:43:59 2017 +0200 +++ b/src/Pure/Thy/html.scala Wed May 31 21:37:50 2017 +0200 @@ -142,6 +142,8 @@ def image(src: String, alt: String = ""): XML.Elem = XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) + def source(src: String): XML.Elem = css_class("source")(div(List(pre(text(src))))) + def style(s: String): XML.Elem = XML.elem("style", text(s)) @@ -202,41 +204,4 @@ init_dir(dir) File.write(dir + Path.basic(name), output_document(head, body, css)) } - - - /* Isabelle document */ - - def begin_document(title: String): String = - header + "\n" + - "\n" + output(head_meta) + "\n" + - "