unicode \begin{verbatim} with cmtt?

Question

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?

Answer 1

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.

Answer 2

The question is now answered. If there aren't many symbols, you can use newunicodechar package to manually map unicode characters to LaTeX code.

\usepackage{newunicodechar}
\newunicodechar{⟨}{\ensuremath{\langle}}

Answer 3

I usually do like this:

\usepackage[utf8]{inputenc}
\usepackage{verbatim}

{\scriptsize \verbatiminput{fileToInput.txt}}

Maybe \verbatiminput does the work for you?

/Have fun