The commands that set them up as syntax should also set up the standard TeX
override map to do this. For example, boolScript.sml includes the following
lines to set up if-then-else:
val _ = TeX_notation {hol = "if", TeX = ("\\HOLKeyword{if}", 2)}
val _ = TeX_notation {hol = "then", TeX
When I make a munger with monadsyntax and use it to typeset some monadic
functions, the "do" and "od" delimiters of a list of binds are emitted
as-is. I would like them to be annotated as HOLKeywords.
I know I could probably use the override map for that, but it seems like
there ought to be a more
