By default the munger doesn't do anything special to strings; the usual
pretty-printing behaviour is to print the elements of the string without
any separators between double-quotes. In math mode, the contents of the
string thus are treated as LaTeX variables and appear in italics with too
much space.
Any ideas on a good way to make the munger wrap the contents of a string,
perhaps with a new \HOLString command?
My guess is this probably requires removing whatever rule pretty-prints
strings and putting in a new one, but if there's anything less heavy-weight
that could be done I'd be happy to know about it.
------------------------------------------------------------------------------
Want fast and easy access to all the code in your enterprise? Index and
search up to 200,000 lines of code with a free copy of Black Duck
Code Sight - the same software that powers the world's largest code
search on Ohloh, the Black Duck Open Hub! Try it now.
http://p.sf.net/sfu/bds
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
