他のソースコードは listings で埋め込んでいたけれど、Agdaで使っている特定の文字が化けて表示されない。
verbatim でも表示されないので、Agda のソースを LaTeX 用にエスケープして、記号処理は LaTeX に任せることで listings できるようになったお話。
環境
- Mac OS X 10.9.5
- MacTeX 20140525
埋め込み方法
listings の escapechar を設定して、表示されない記号を LaTeX 用に置換してあげる。
escapechar が @ で、≡ を置換したかったら @$\equiv$@ みたいな。
escapechar の中は LaTeX 環境になるので、$ で数式を直接書いてしまえばok。
スクリプトとかは以下。
.agda から置換した .eagda を生成してくれます。
LaTeX からの参照は .eagda を指定してます。
escapechar の中は LaTeX 環境になるので、$ で数式を直接書いてしまえばok。
スクリプトとかは以下。
.agda から置換した .eagda を生成してくれます。
LaTeX からの参照は .eagda を指定してます。
周り道とか
Literate Agda ってのもあるみたいです。
lagda で書いておけば LaTeX としても認識してくれるっぽい?
でも今回は使わない方向でいきました。
本来Agdaのソースを埋め込むのならこっちなのかな。
あと大きなソース(500行くらい)のやつを LaTeX に食わせるとメモリが足りなくて落ちる時が。
とか言われる。! TeX capacity exceeded, sorry [main memory size=5000000].
/usr/local/texlive/2014/texmf.cnf に
main_memory=8000000とか書いたら動いた。
extra_mem_bot=8000000
font_mem_size=8000000
pool_size=8000000
buf_size=8000000
メモリの制限とか自前で持ってるのね TeX。
あと、utf8周りでもメモリ周りでも LuaTeX 良いよって指摘があった。
LuaTeX 使うのも良いのかもしれない。
ちなみに今回は platex 使いました。
あとは listings 側のオプションに escapeinside とか literate とか使えそうなのもあったけれど動かず。
これはどうしてなのだろう。
ウムラウト付きの文字なら literate できます、みたいなのは記事にあったんだけれど ≡ は置換されず。
0 件のコメント:
コメントを投稿