# HG changeset patch
# User wenzelm
# Date 1446898403 -3600
# Node ID ed4dad8823a44ed814bb38af553da539a6a94bb0
# Parent  53e32a9b66b8834dfb19186c85fdb8fd812c15e1
less confusing markup;

diff -r 53e32a9b66b8 -r ed4dad8823a4 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sat Nov 07 12:53:22 2015 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Sat Nov 07 13:13:23 2015 +0100
@@ -12,9 +12,8 @@
 val _ = Theory.setup
  (ML_Antiquotation.value @{binding cartouche}
     (Args.context -- Scan.lift (Parse.position Args.cartouche_input) >> (fn (ctxt, (source, pos)) =>
-      (Context_Position.report ctxt pos Markup.ML_cartouche;
-        "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
-          ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source))))) #>
+      "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
+        ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #>
 
   ML_Antiquotation.inline @{binding undefined}
     (Scan.succeed "(raise General.Match)") #>
diff -r 53e32a9b66b8 -r ed4dad8823a4 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Nov 07 12:53:22 2015 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Nov 07 13:13:23 2015 +0100
@@ -101,7 +101,6 @@
   val ML_numeralN: string val ML_numeral: T
   val ML_charN: string val ML_char: T
   val ML_stringN: string val ML_string: T
-  val ML_cartoucheN: string val ML_cartouche: T
   val ML_commentN: string val ML_comment: T
   val SML_stringN: string val SML_string: T
   val SML_commentN: string val SML_comment: T
@@ -440,7 +439,6 @@
 val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
 val (ML_charN, ML_char) = markup_elem "ML_char";
 val (ML_stringN, ML_string) = markup_elem "ML_string";
-val (ML_cartoucheN, ML_cartouche) = markup_elem "ML_cartouche";
 val (ML_commentN, ML_comment) = markup_elem "ML_comment";
 val (SML_stringN, SML_string) = markup_elem "SML_string";
 val (SML_commentN, SML_comment) = markup_elem "SML_comment";
diff -r 53e32a9b66b8 -r ed4dad8823a4 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Nov 07 12:53:22 2015 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Nov 07 13:13:23 2015 +0100
@@ -260,7 +260,6 @@
   val ML_NUMERAL = "ML_numeral"
   val ML_CHAR = "ML_char"
   val ML_STRING = "ML_string"
-  val ML_CARTOUCHE = "ML_cartouche"
   val ML_COMMENT = "ML_comment"
   val SML_STRING = "SML_string"
   val SML_COMMENT = "SML_comment"
diff -r 53e32a9b66b8 -r ed4dad8823a4 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)