isabelle-jedit.css: suppress "location" markup, which indicates extra positional information intended for plain-old TTY mode;
authorwenzelm
Wed, 08 Sep 2010 23:40:48 +0200
changeset 39229 6530e87186c9
parent 39228 cb7264721c91
child 39230 184507f6e8d0
isabelle-jedit.css: suppress "location" markup, which indicates extra positional information intended for plain-old TTY mode;
src/Tools/jEdit/dist-template/etc/isabelle-jedit.css
--- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Wed Sep 08 23:34:40 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Wed Sep 08 23:40:48 2010 +0200
@@ -8,6 +8,8 @@
 .error { background-color: #FFC1C1; }
 .debug { background-color: #FFE4E1; }
 
+.location { display: none; }
+
 .hilite { background-color: #FFFACD; }
 
 .keyword { font-weight: bold; color: #009966; }