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, "")