Just for the archives, in case anyone else has this problem:

a check/tick mark, ✓ is UTF U+2713 and is shown inTeXmacs with \<checkmark\> but this often doesn't work but instead shows <checkkmark> in red.

This macro will display it for you by selecting the correct font/font family:

<assign|tick|<macro|<with|font|modern|font-family|ss|\<checkmark\>>>>>

However this one will not:
<assign|checkmark|<macro|<with|font|modern|font-family|ss|\<checkmark\>>>>

because typing \checkmark generates the entity \<checkmark\> instead of the macro invocation <checkmark>

but typing \compound ENTER checkmark ENTER will invoke the macro but will not fixup existing checkmark entities in the document.

So... you may as well use a plain out-and-out macro with a different name to invoke the checkmark entity with the right font.


(I'm sure tex is good at changing font when needed to display symbols).

Sam