src/Pure/PIDE/rendering.scala
changeset 74887 56247fdb8bbb
parent 74782 0a87ea7eb76f
child 75393 87ebf5a50283
--- a/src/Pure/PIDE/rendering.scala	Mon Dec 06 15:10:15 2021 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Dec 06 15:34:54 2021 +0100
@@ -117,7 +117,6 @@
     Markup.OPERATOR -> Color.operator,
     Markup.STRING -> Color.main,
     Markup.ALT_STRING -> Color.main,
-    Markup.VERBATIM -> Color.main,
     Markup.CARTOUCHE -> Color.main,
     Markup.LITERAL -> Color.keyword1,
     Markup.DELIMITER -> Color.main,
@@ -151,7 +150,6 @@
     Map(
       Markup.STRING -> Color.quoted,
       Markup.ALT_STRING -> Color.quoted,
-      Markup.VERBATIM -> Color.quoted,
       Markup.CARTOUCHE -> Color.quoted,
       Markup.ANTIQUOTED -> Color.antiquoted)
 
@@ -209,7 +207,7 @@
     Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
 
   val language_context_elements =
-    Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
+    Markup.Elements(Markup.STRING, Markup.ALT_STRING,
       Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
       Markup.ML_STRING, Markup.ML_COMMENT)