--- a/src/Pure/Thy/html.scala Sat Nov 09 11:24:21 2013 +0100 +++ b/src/Pure/Thy/html.scala Sat Nov 09 11:41:32 2013 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/Thy/html.scala + Module: PIDE-GUI Author: Makarius HTML presentation elements.