2015/03/01

Agda のソースコードを listings で LaTeX に埋め込む

LaTeX で Agda のソースコードを含む pdf を作ることに。
他のソースコードは 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 を指定してます。




周り道とか

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 件のコメント:

コメントを投稿