tuned markup;
authorwenzelm
Tue, 28 Jun 2011 20:42:29 +0200
changeset 43589 8e3e933b3c69
parent 43588 ad4e860fd28b
child 43590 0940a64beca2
tuned markup;
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(