* TikZ output: see misc/DrawTikZ.py.