# HG changeset patch # User krauss # Date 1306361550 -7200 # Node ID a59db667752178c40f708a304f04f831a638217b # Parent 9901f877eeb729e1f51c2807ccbdc149a5af31ee css rules for highlighting sendback text diff -r 9901f877eeb7 -r a59db6677521 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; }