src/Tools/jEdit/src/rendering.scala

--- a/src/Tools/jEdit/src/rendering.scala	Sat Nov 07 12:53:22 2015 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Nov 07 13:13:23 2015 +0100
@@ -143,7 +143,7 @@
   private val language_context_elements =
     Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
       Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
-      Markup.ML_STRING, Markup.ML_CARTOUCHE, Markup.ML_COMMENT)
+      Markup.ML_STRING, Markup.ML_COMMENT)
 
   private val language_elements = Markup.Elements(Markup.LANGUAGE)
 
@@ -309,9 +309,7 @@
           if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
           else None
         case Text.Info(_, elem)
-        if elem.name == Markup.ML_STRING ||
-          elem.name == Markup.ML_CARTOUCHE ||
-          elem.name == Markup.ML_COMMENT =>
+        if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
           Some(Completion.Language_Context.ML_inner)
         case Text.Info(_, _) =>
           Some(Completion.Language_Context.inner)
@@ -778,7 +776,6 @@
       Markup.ML_NUMERAL -> inner_numeral_color,
       Markup.ML_CHAR -> inner_quoted_color,
       Markup.ML_STRING -> inner_quoted_color,
-      Markup.ML_CARTOUCHE -> inner_cartouche_color,
       Markup.ML_COMMENT -> inner_comment_color,
       Markup.SML_STRING -> inner_quoted_color,
       Markup.SML_COMMENT -> inner_comment_color)