# HG changeset patch
# User wenzelm
# Date 1495833710 -7200
# Node ID 9fb044904a4d8f1abc0f32538ab4d58311947b71
# Parent  1b297ce1e8aa38cee48954cddd2f93ebb2c11756
support for message underline and tooltips;

diff -r 1b297ce1e8aa -r 9fb044904a4d etc/isabelle.css
--- a/etc/isabelle.css	Fri May 26 21:40:52 2017 +0200
+++ b/etc/isabelle.css	Fri May 26 23:21:50 2017 +0200
@@ -85,3 +85,37 @@
 .warning_message      { background-color: #EEE8AA; }
 .legacy_message       { background-color: #EEE8AA; }
 .error_message        { background-color: #FFC1C1; }
+
+
+/* message underline */
+
+.writeln { border-bottom: 1px dotted #C0C0C0; }
+.information { border-bottom: 1px dotted #C1DFEE; }
+.warning { border-bottom: 1px dotted #FF8C00; }
+.legacy { border-bottom: 1px dotted #FF8C00; }
+.error { border-bottom: 1px dotted #B22222; }
+
+
+/* tooltips */
+
+.writeln { position: relative; display: inline-block; }
+.information { position: relative; display: inline-block; }
+.warning { position: relative; display: inline-block; }
+.legacy { position: relative; display: inline-block; }
+.error { position: relative; display: inline-block; }
+
+.writeln:hover .tooltip { visibility: visible; }
+.information:hover .tooltip { visibility: visible; }
+.warning:hover .tooltip { visibility: visible; }
+.legacy:hover .tooltip { visibility: visible; }
+.error:hover .tooltip { visibility: visible; }
+
+.tooltip {
+  visibility: hidden;
+  width: 40em;
+  border: 1px solid #808080;
+  padding: 3px 3px;
+  background-color: #FFFFE9;
+  position: absolute;
+  z-index: 1;
+}
diff -r 1b297ce1e8aa -r 9fb044904a4d src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Fri May 26 21:40:52 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Fri May 26 23:21:50 2017 +0200
@@ -262,7 +262,7 @@
             (data_entry.failed_sessions match {
               case Nil => Nil
               case sessions =>
-                HTML.break ::: List(HTML.error_message_span("Failed:")) :::
+                HTML.break ::: List(HTML.span(HTML.text("Failed:")) + HTML.error_message_class) :::
                 HTML.text(" " +
                   commas(sessions.map(s => s.name + " (" + s.head.isabelle_version + ")")))
             })
diff -r 1b297ce1e8aa -r 9fb044904a4d src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Fri May 26 21:40:52 2017 +0200
+++ b/src/Pure/Thy/html.scala	Fri May 26 23:21:50 2017 +0200
@@ -140,17 +140,18 @@
 
   /* messages */
 
+  // background
   val writeln_message_class: XML.Attribute = css_class("writeln_message")
   val warning_message_class: XML.Attribute = css_class("warning_message")
   val error_message_class: XML.Attribute = css_class("error_message")
 
-  def writeln_message(msg: String): XML.Elem = par(text(msg)) + writeln_message_class
-  def warning_message(msg: String): XML.Elem = par(text(msg)) + warning_message_class
-  def error_message(msg: String): XML.Elem = par(text(msg)) + error_message_class
+  // underline
+  val writeln_class: XML.Attribute = css_class("writeln")
+  val warning_class: XML.Attribute = css_class("warning")
+  val error_class: XML.Attribute = css_class("error")
 
-  def writeln_message_span(msg: String): XML.Elem = span(text(msg)) + writeln_message_class
-  def warning_message_span(msg: String): XML.Elem = span(text(msg)) + warning_message_class
-  def error_message_span(msg: String): XML.Elem = span(text(msg)) + error_message_class
+  // tooltips
+  val tooltip_class: XML.Attribute = css_class("tooltip")
 
 
   /* document */