named_deco_struct deco_table[] = {
// Decorations
- {"widehat", angle, 3 },
- {"widetilde", tilde, 0 },
- {"underline", hline, 0 },
- {"overline", hline, 0 },
- {"underbrace", brace, 1 },
- {"overbrace", brace, 3 },
- {"overleftarrow", arrow, 1 },
+ {"widehat", angle, 3 },
+ {"widetilde", tilde, 0 },
+ {"underline", hline, 0 },
+ {"overline", hline, 0 },
+ {"underbrace", brace, 1 },
+ {"overbrace", brace, 3 },
+ {"overleftarrow", arrow, 1 },
{"overrightarrow", arrow, 3 },
// Delimiters
- {"(", parenth, 0 },
- {")", parenth, 2 },
- {"{", brace, 0 },
- {"}", brace, 2 },
- {"[", brack, 0 },
- {"]", brack, 2 },
- {"|", vert, 0 },
- {"/", slash, 0 },
- {"Vert", Vert, 0 },
- {"'", slash, 1 },
- {"langle", angle, 0 },
- {"lceil", corner, 0 },
- {"lfloor", corner, 1 },
- {"rangle", angle, 2 },
- {"rceil", corner, 3 },
- {"rfloor", corner, 2 },
- {"downarrow", arrow, 2 },
- {"Downarrow", Arrow, 2 },
- {"uparrow", arrow, 0 },
- {"Uparrow", Arrow, 0 },
- {"updownarrow", udarrow, 0 },
- {"Updownarrow", Udarrow, 0 },
-
- // Accents
- {"ddot", hline2, 0 },
- {"hat", angle, 3 },
- {"grave", slash, 1 },
- {"acute", slash, 0 },
- {"tilde", tilde, 0 },
- {"bar", hline, 0 },
- {"dot", hlinesmall, 0 },
- {"check", angle, 1 },
- {"breve", parenth, 1 },
- {"vec", arrow, 3 },
- {"not", slash, 0 },
-
- // Dots
- {"ldots", hline3, 0 },
- {"cdots", hline3, 0 },
- {"vdots", hline3, 1 },
- {"ddots", dline3, 0 }
+ {"(", parenth, 0 },
+ {")", parenth, 2 },
+ {"{", brace, 0 },
+ {"}", brace, 2 },
+ {"[", brack, 0 },
+ {"]", brack, 2 },
+ {"|", vert, 0 },
+ {"/", slash, 0 },
+ {"Vert", Vert, 0 },
+ {"'", slash, 1 },
+ {"langle", angle, 0 },
+ {"lceil", corner, 0 },
+ {"lfloor", corner, 1 },
+ {"rangle", angle, 2 },
+ {"rceil", corner, 3 },
+ {"rfloor", corner, 2 },
+ {"downarrow", arrow, 2 },
+ {"Downarrow", Arrow, 2 },
+ {"uparrow", arrow, 0 },
+ {"Uparrow", Arrow, 0 },
+ {"updownarrow", udarrow, 0 },
+ {"Updownarrow", Udarrow, 0 },
+
+ // Accents
+ {"ddot", hline2, 0 },
+ {"hat", angle, 3 },
+ {"grave", slash, 1 },
+ {"acute", slash, 0 },
+ {"tilde", tilde, 0 },
+ {"bar", hline, 0 },
+ {"dot", hlinesmall, 0 },
+ {"check", angle, 1 },
+ {"breve", parenth, 1 },
+ {"vec", arrow, 3 },
+ {"not", slash, 0 },
+
+ // Dots
+ {"ldots", hline3, 0 },
+ {"cdots", hline3, 0 },
+ {"vdots", hline3, 1 },
+ {"ddots", dline3, 0 }
};