--- a/src/Pure/General/symbol.scala Mon Nov 19 15:32:12 2018 +0100
+++ b/src/Pure/General/symbol.scala Tue Nov 20 13:44:06 2018 +0100
@@ -135,6 +135,12 @@
def trim_blanks(text: CharSequence): String =
Library.trim(is_blank(_), explode(text)).mkString
+ def all_blank(str: String): Boolean =
+ iterator(str).forall(is_blank(_))
+
+ def trim_blank_lines(text: String): String =
+ cat_lines(split_lines(text).dropWhile(all_blank).reverse.dropWhile(all_blank).reverse)
+
/* decoding offsets */
--- a/src/Pure/Thy/present.scala Mon Nov 19 15:32:12 2018 +0100
+++ b/src/Pure/Thy/present.scala Tue Nov 20 13:44:06 2018 +0100
@@ -55,9 +55,10 @@
List(HTML.div("sessions",
List(HTML.description(
sessions.map({ case (name, description) =>
+ val descr = Symbol.trim_blank_lines(description)
(List(HTML.link(name + "/index.html", HTML.text(name))),
- if (description == "") Nil
- else HTML.break ::: List(HTML.pre(HTML.text(description)))) })))))))
+ if (descr == "") Nil
+ else HTML.break ::: List(HTML.pre(HTML.text(descr)))) })))))))
}
def make_global_index(browser_info: Path)