# HG changeset patch
# User wenzelm
# Date 1283982048 -7200
# Node ID 6530e87186c95c359fa3a312b85dccc992b580e6
# Parent  cb7264721c916b4322a3f342ab5429ac7587a321
isabelle-jedit.css: suppress "location" markup, which indicates extra positional information intended for plain-old TTY mode;

diff -r cb7264721c91 -r 6530e87186c9 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; }