diff -r b49366215417 -r 8e8243975860 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Jan 17 20:51:36 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Jan 18 19:15:12 2014 +0100
@@ -59,6 +59,7 @@
   val literalN: string val literal: T
   val delimiterN: string val delimiter: T
   val inner_stringN: string val inner_string: T
+  val inner_cartoucheN: string val inner_cartouche: T
   val inner_commentN: string val inner_comment: T
   val token_rangeN: string val token_range: T
   val sortN: string val sort: T
@@ -92,6 +93,7 @@
   val stringN: string val string: T
   val altstringN: string val altstring: T
   val verbatimN: string val verbatim: T
+  val cartoucheN: string val cartouche: T
   val commentN: string val comment: T
   val controlN: string val control: T
   val tokenN: string val token: Properties.T -> T
@@ -307,6 +309,7 @@
 val (literalN, literal) = markup_elem "literal";
 val (delimiterN, delimiter) = markup_elem "delimiter";
 val (inner_stringN, inner_string) = markup_elem "inner_string";
+val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche";
 val (inner_commentN, inner_comment) = markup_elem "inner_comment";
 
 val (token_rangeN, token_range) = markup_elem "token_range";
@@ -361,6 +364,7 @@
 val (stringN, string) = markup_elem "string";
 val (altstringN, altstring) = markup_elem "altstring";
 val (verbatimN, verbatim) = markup_elem "verbatim";
+val (cartoucheN, cartouche) = markup_elem "cartouche";
 val (commentN, comment) = markup_elem "comment";
 val (controlN, control) = markup_elem "control";