--- 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; }
--- 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<div class=\"source\">\n<pre class=\"source\">" +
- HTML.output(Symbol.decode(File.read(Path.explode("~~/NEWS")))) +
- "</pre>\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"))))))
}
--- 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" +
- "<head>\n" + output(head_meta) + "\n" +
- "<title>" + output(title + " (" + Distribution.version + ")") + "</title>\n" +
- "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" +
- "</head>\n" +
- "\n" +
- "<body>\n" +
- "<div class=\"head\">" +
- "<h1>" + output(title) + "</h1>\n"
-
- val end_document = "\n</div>\n</body>\n</html>\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 "<div class=\"sessions\"><ul>\n" + sessions.map(session_entry(_)).mkString + "</ul>") +
- end_document
- }
}
--- 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)