A lot of leading-edge programming languages (like Coq and Agda) allow nearly unrestricted use of unicode symbols in program text, so you can have math characters like $\otimes$ (Unicode U+2A02) as operators in your program.
I'd like to be able to cut and paste these programs directly into my LaTeX documents inside a verbatim-like environment and get a reasonable result. For various reasons I can't use the listings environment — I need the typeset output to look the same as the program looks on the computer screen, even if the listings package would make it "prettier".
Unfortunately the computer modern typewriter (cmtt) font, which I really like a lot, doesn't have math symbols, but there ought to be some package that acts like verbatim using cmtt wherever possible and falls back to the math fonts when it encounters a unicode symbol that isn't in cmtt.
A package like this would probably require a major effort to "line up" the unicode math symbols with the Latex Symbols List, but once a table like that were to be compiled it would be really, really useful!
So, I guess my question is in two parts: has anybody compiled such a table, and (more importantly) has anybody used it to produce a verbatim that makes a "reasonable effort" at handling unicode math characters?
Best Answer
I recommend using either XeLaTeX or LuaLaTeX and loading an appropriate Unicode font for the verbatim that requires those symbols. pdfLaTeX won't cut it in this case, I'm afraid.