# 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 */