Agdaとフォントと微妙な設定

Agda書くとみんなフォントに困る…と,思う.Agda標準ライブラリの時点で_⊔_とか_⊎_とか⟨_⟩とか普通のランゲッジでは使わないような文字入りの演算が目白押しだ.当然下手なフォント設定すると正しく表示されない.プログラミングに適したmonospaceのフォントでこういうのをフォローできてるスケーラブルフォントが欲しい.

聞くところによるとWindowsユーザはWindowsインストーラ版を使うとあんまり気になることない(GNU unifontもワンセットで入るから?)らしい.でもGNU unifontってビットマップフォントのようだし,putty仮想マシンGentoo入ってX無しでサギョウ…という私のカッコイイスタイルでは使えない.そもそもWindowsインストーラ版のAgdaなど花拳繍腿.一度汚れたWindowsはもう二度と元には…元には…なので,あんまりWindowsに余計なもの入れたくはないし.

で,結局どうしてるかというところだが.ザックリDejaVu Sans MonoにMS UI GothicをFontLinkして使っている.

FontLinkとはWindowsのステキ機能()で,あるフォントに欠けてる文字を別に指定したフォントから持ってきてカバーするような機能だ.レジストリを弄る.HKEY_LOCAL_MACHINE\SOFTWARE\Microsoft\Windows NT\CurrentVersion\FontLink\SystemLink 以下にメインのフォント名の値を追加し,データとして"フォントファイル,フォント名,表示アスペクト比?(スケール,スケール)"という値を必要なだけ記述する.次のような感じ.

レジストリ: HKEY_LOCAL_MACHINE\SOFTWARE\Microsoft\Windows NT\CurrentVersion\FontLink\SystemLink
値: DejaVu Sans Mono
種類: REG_MULTI_SZ
データ:
MSGOTHIC.TTC,MS UI Gothic,128,80

レジストリ弄ってるなら結局汚してるじゃねーかというのはもっともではあるが…汚されているんでなく汚してるんだし(震え声)

で,これ.主な問題は最後の数字2つの調整で,これらの値,何が正しくてどう調整すればいいのか自分には全くわからない(まあ,Windowsの話なのであんまり理解する気も無いのだが).メインのフォント(この場合DejaVu Sans Mono)に合わせるためのものなので,それによって設定されるべき値も違ってくる.下手な値にするとどうなるかというと,FontLineによって出張ってきた(MS UI Gothicの)文字がスゴイ横にツブれた文字になったり,上半分が切れて表示されたりとかする.しかもレジストリ値なので設定変たらリブート,それでもダメならまた変えてリブートと非常にメンドクサイ2分探索を強いられる.恐しいことにアプリケーションによっても影響が異なり,この設定はputty合わせで行ったが,sakura editorで見たらなんかダメだった(まぁ,これはCJK ambiguous charactersの扱いが違うとか別要因もあるかも).

他のひとたちはどうしてるんだろうというのは実際興味ある.たぶんnativeなlinuxとかmacとかなんだろうけどね.macもあんまりよく知らないけどMBAのiTerm上からMonacoで同様に仮想マシン入ってAgdaする分にはあんまりフォント問題無いようだし.