# 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
\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" + - "" + output(title + " (" + Distribution.version + ")") + "\n" + - "\n" + - "\n" + - "\n" + - "\n" + - "
" + - "

" + output(title) + "

\n" - - val end_document = "\n
\n\n\n" - - - /* common markup elements */ - - private def session_entry(entry: (String, String)): String = - { - val (name, description) = entry - val descr = if (description == "") Nil else break ::: List(pre(text(description))) - XML.string_of_tree( - XML.elem("li", - List(XML.Elem(Markup("a", List(("href", name + "/index.html"))), - List(XML.Text(name)))) ::: descr)) + "\n" - } - - def chapter_index(chapter: String, sessions: List[(String, String)]): String = - { - begin_document("Isabelle/" + chapter + " sessions") + - (if (sessions.isEmpty) "" - else "
") + - end_document - } } diff -r 44e44bfc738a -r 8040d2563593 src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Wed May 31 20:43:59 2017 +0200 +++ b/src/Pure/Thy/present.scala Wed May 31 21:37:50 2017 +0200 @@ -16,7 +16,6 @@ { /* maintain chapter index -- NOT thread-safe */ - private val index_path = Path.basic("index.html") private val sessions_path = Path.basic(".sessions") private def read_sessions(dir: Path): List[(String, String)] = @@ -45,9 +44,20 @@ catch { case _: XML.Error => Nil } val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList + write_sessions(dir, sessions) - write_sessions(dir, sessions) - File.write(dir + index_path, HTML.chapter_index(chapter, sessions)) + val title = "Isabelle/" + chapter + " sessions" + HTML.write_document(dir, "index.html", + List(HTML.title(title + " (" + Distribution.version + ")")), + HTML.chapter(title) :: + (if (sessions.isEmpty) Nil + else + List(HTML.css_class("sessions")(HTML.div(List( + HTML.itemize( + sessions.map({ case (name, description) => + HTML.link(name + "/index.html", HTML.text(name)) :: + (if (description == "") Nil + else List(HTML.pre(HTML.text(description)))) })))))))) } def make_global_index(browser_info: Path)