# 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(