# HG changeset patch
# User wenzelm
# Date 1542717846 -3600
# Node ID f3351bb4390e5019ae25a7add09bddf186bf0775
# Parent  e8dea06456b4129dcf0626d267ff6b4b4253d03f
clarified presentation;

diff -r e8dea06456b4 -r f3351bb4390e src/Pure/General/symbol.scala
--- 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 */
 
diff -r e8dea06456b4 -r f3351bb4390e src/Pure/Thy/present.scala
--- 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)