css rules for highlighting sendback text
authorkrauss
Thu, 26 May 2011 00:12:30 +0200
changeset 42977 a59db6677521
parent 42976 9901f877eeb7
child 42978 6b41a075251f
css rules for highlighting sendback text
src/Tools/jEdit/dist-template/etc/isabelle-jedit.css
--- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Thu May 26 00:12:01 2011 +0200
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Thu May 26 00:12:30 2011 +0200
@@ -15,3 +15,5 @@
 .operator { font-weight: bold; }
 .command { font-weight: bold; color: #006699; }
 
+.sendback { text-decoration: underline; }
+.sendback:hover { background-color: #FFCC66; }