AgdaでTex、そして日本語 その2

とりあえず、LuaLaTeX上でLuaTeX-jaパッケージを動かして、日本語表示とunicodeのマニアックな記号表示を両立されるところまではできたぞ。環境はWindows7上のTeXWorks。

成果物はGithubに

• https://github.com/kino3/luatex-ja

フォントの制御はまだうまくできていないが、unicodeの記号および日本語はPDFで表示できるようになった。とりあえず一段落。

見たサイト

• http://zrbabbler.sp.land.to/lualatexuni.html
• http://sourceforge.jp/projects/luatex-ja/wiki/LuaTeX-ja%E3%81%AE%E4%BD%BF%E3%81%84%E6%96%B9
• http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda

まだよくわからん

• unicode部分のフォント指定。いまは日本語フォント（上記PDFではMSゴシック）になっているようだが・・・
  • http://ctan.math.washington.edu/tex-archive/macros/latex/contrib/fontspec/fontspec.pdf あたりをきちんと読む必要がある。
  • 気持ちとしては、Emacsのようにこのコードからこのコードまではこのフォント、とできたらいいのだが。それか、書いてあるところにいちいち直接フォント名指定、ということなのかな。

このあとやる

• lagdaファイルを使ったAgdaコードつき日本語文書のPDF化（Literate Agda）
• フォントをいい感じにする
  • https://github.com/yascentur/Ricty これ試してみたい。