diff -r c3d02b3518c2 -r 6ac3c29a300e src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Mon Mar 11 14:25:14 2013 +0100 +++ b/src/Pure/Thy/html.scala Tue Mar 12 16:47:24 2013 +0100 @@ -11,7 +11,7 @@ object HTML { - // encode text + /* encode text */ def encode(text: String): String = { @@ -29,7 +29,27 @@ } - // common markup elements + /* document */ + + val end_document = "\n\n\n\n" + + def begin_document(title: String): String = + "\n" + + "\n" + + "\n" + + "\n" + + "\n" + + "" + encode(title) + "\n" + + "\n" + + "\n" + + "\n" + + "\n" + + "
" + + "

" + encode(title) + "

\n" + + + /* common markup elements */ def session_entry(name: String): String = XML.string_of_tree( @@ -37,11 +57,11 @@ List(XML.Elem(Markup("a", List(("href", name + "/index.html"))), List(XML.Text(name)))))) + "\n" - def session_entries(names: List[String]): String = - if (names.isEmpty) "" - else - "\n
\n
\n" + - "

Sessions

\n"; - - val end_document = "\n
\n\n\n" + def chapter_index(chapter: String, sessions: List[String]): String = + { + begin_document("Isabelle/" + chapter + " sessions") + + (if (sessions.isEmpty) "" + else "
") + + end_document + } }