src/Pure/Thy/thy_syntax.ML
changeset 55033 8e8243975860
parent 54520 cee77d2e9582
child 55118 7df949045dc5
--- a/src/Pure/Thy/thy_syntax.ML	Fri Jan 17 20:51:36 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Sat Jan 18 19:15:12 2014 +0100
@@ -56,6 +56,7 @@
   | Token.String        => (Markup.string, "")
   | Token.AltString     => (Markup.altstring, "")
   | Token.Verbatim      => (Markup.verbatim, "")
+  | Token.Cartouche     => (Markup.cartouche, "")
   | Token.Space         => (Markup.empty, "")
   | Token.Comment       => (Markup.comment, "")
   | Token.InternalValue => (Markup.empty, "")