# HG changeset patch
# User wenzelm
# Date 1309286549 -7200
# Node ID 8e3e933b3c69fff3c5ec85f78f14aad4cf4278fa
# Parent  ad4e860fd28baffba2e35cdc964e8aebf59dda84
tuned markup;

diff -r ad4e860fd28b -r 8e3e933b3c69 src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Tue Jun 28 17:13:32 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Tue Jun 28 20:42:29 2011 +0200
@@ -114,10 +114,7 @@
     Map(
       Markup.CLASS -> get_color("red"),
       Markup.TYPE -> get_color("black"),
-      Markup.CONSTANT -> get_color("black"),
-      Markup.ML_ANTIQUOTATION -> get_color("black"),
-      Markup.DOCUMENT_ANTIQUOTATION -> get_color("black"),
-      Markup.DOCUMENT_ANTIQUOTATION_OPTION -> get_color("black"))
+      Markup.CONSTANT -> get_color("black"))
 
   private val text_colors: Map[String, Color] =
     Map(