ProofGeneralの起動画面のカスタマイズについて

小ネタです。ProofGeneralの起動画面を見ただけで気分が盛り上がるようにしてみよう。

今年の.emacs Advent Calendar 2016にあるEmacsの起動画面のカスタマイズについてを読んで書きたくなりました。

ProofGeneralは、対話的定理証明系(interactive theorem prover)のEmacsで動くフロントエンドです。

執筆時のProofGeneralのバージョンはversion 4.4.1~preです。ProofGeneralをバージョンアップしたあとは、
この記事にある設定ではうまくいかなくなるかもしれません。

スクリーンショット

デフォルトのProofGeneralの起動画面です。
じぇねらるたん(Generaltan)はProofGeneralの公式ロゴです。

メリークリスマス！

ロゴ画像の変更

ロゴ画像を変更する方法です。画像を置くディレクトリと画像ファイル名をそれぞれ指定してください。

  (require 'proof-site)
  (require 'proof-splash)

  (defvar my/proof-logo-image-directory
	proof-images-directory
	"Where the logo image of Proof General is. Ends with slash.")

  (defvar my/proof-logo-image-file-name
	"ProofGeneral-splash.png"
	"The file name of the PNG logo image of Proof General.")

  ;; 各自が設定を書くところ
  (setq my/proof-logo-image-directory
    ;; ロゴを置いたディレクトリ
    ;; 絶対パスであること（相対パスではだめ）
    ;; 先頭が~ではじまってもよい（ホームディレクトリを使うときは）
    ;; 末尾は/で終わること
    "ディレクトリの名前")
  (setq my/proof-logo-image-file-name
    ;; ロゴ画像のファイル名
    ;; 画像はPNGフォーマットにすること
    "ファイル名.png")
  ;; 各自の設定、ここまで

  (defun my/proof-get-image (dir name)
    "Absolutely similar to the function `proof-get-image`."
    (if (display-graphic-p)
        (find-image
         `((:type png :file
                  ,(expand-file-name name dir))))
      (concat "[ image " name " ]")))

  (setq proof-splash-contents
        (append
         '(list (my/proof-get-image
                 my/proof-logo-image-directory
                 my/proof-logo-image-file-name))
         (cdr (cdr proof-splash-contents))))

PNG形式でないロゴ画像を使いたいときは、上で定義した関数my/proof-get-imageのなかのpngを適切に変えることで実現できます。

Emacsの設定を変更する方法はEmacsのバージョンとか個々人のカスタマイズのスタイルによって違います。

設定ファイル~/.emacs.d/init.elのなかでsetqする
設定ファイル~/.emacs あるいは~/.emacs.elのなかでsetqする
その他

が考えられます。僕は~/.emacs.d/init.elに設定を書いています。
.emacs Advent Calendar 2016の記事
.emacsなの?.emacs.elなの?init.elなの?
が参考になるでしょう。

おまけ

ProofGeneralの起動画面を表示しない

;; 起動画面を表示しない
(setq proof-splash-enable nil)

デフォルトは起動画面を表示する

ProofGeneralの起動画面の表示時間を変える

;; たとえば5秒
(setq proof-splash-time 5)

起動画面の表示時間のデフォルトは最低8秒

起動画面のレイアウトをかえたい

ロゴ画像を変えるだけでなく、レイアウトをもっと変えたいと思うひとのためにしくみも書きます。

解説

ProofGeneralが参照するEmacs Lispのカスタマイズ変数proof-splash-contentsのデフォルトをgeneric/proof-splash.elから抜粋します。

  '(list
     (proof-get-image "ProofGeneral-splash.png")
      nil
      "Welcome to"
      (concat proof-assistant " Proof General!")
      nil
      (concat "Version " proof-general-short-version ".")
      nil
      (concat "© LFCS, University of Edinburgh & contributors "
        proof-general-version-year)
      nil
      nil
      :link '("    Read the "
              "Proof General documentation"
              (lambda (button) (info "ProofGeneral")))
      :link '("    Please report problems on the "
              "Github issue tracker"
	              (lambda (button)
				  (browse-url "https://github.com/ProofGeneral/PG/issues"))
              "Report bugs at https://github.com/ProofGeneral/PG")
			      :link '("Visit the " "Proof General Github page"
	              (lambda (button)
				  (browse-url "https://github.com/ProofGeneral/PG"))
              "PG is on Github at https://github.com/ProofGeneral/PG")
      :link '("or the " "homepage"
	              (lambda (button)
  				  (browse-url "https://proofgeneral.github.io"))
              "Browse https://proofgeneral.github.io")
      nil
      :link '("Find out about Emacs on the Help menu -- start with the "
              "Emacs Tutorial" (lambda (button) (help-with-tutorial)))
      nil
      "See this screen again with Proof-General -> About"
      )

です。

変数proof-splash-contentsは次の情報を保持しています。

画像
文字列
リンク
改行

各要素について簡単に説明します。

画像について。変数proof-splash-contentsは、デフォルトでは画像の取得に関数proof-get-imageを使っています。
proof-get-imageは変数proof-images-directoryに格納されているディレクトリの画像を参照します。ロゴ画像はProofGeneral-splash.pngです。

しかし、ロゴを変更するためにproof-images-directoryを書き換えるのはおすすめできません。というのは、このディレクトリの中にはロゴだけではなく、ProofGeneralが用いるアイコン画像もあるからです。

かといって、ディレクトリproof-images-directoryの中にロゴ画像を入れると、ProofGeneralをバージョンアップしたときに困るかもしれません。関数proof-get-imageの代わりとなる方法を準備したほうがよいと思います。上記に書いた設定例でのmy/proof-get-imageはproof-get-imageの定義の（ほぼ）コピペです。

文字列はProofGeneralの起動画面にそのまま表示されます。

連想リストでリンクを表示します。
この連想リストは、:linkをキーとします。
また、値を、文字列と、1変数からなる関数からなるリストとします。
文字列が被リンク、1変数からなる関数がアクションです。

アクションについてですが、Emacsのinfoを表示したり、Web pageを表示したり、バッファ(Emacs用語)を表示したりできます。アクションは1変数からなる関数でなければいけない、はずです。
具体例を一つ挙げると(lambda (button) (browse-url "https://github.com/ProofGeneral/PG"))でProofGeneralのGitHubリポジトリへのリンク（と、それを開くアクション）が作られます。

最後に。リストの要素nilは起動画面における改行を意味しています。

ロゴ画像入れ替えのしくみ

この記事の先頭に書いた、ロゴ画像の入れ替えの設定のしくみ。proof-splash-contentsのデフォルトの値（リスト）の二番目の要素（ロゴ表示）を、自前の(my/proof-get-image my/proof-lego-image-directory my/proof-lego-image-file-name)に置き換えているだけです。

ここまでのまとめ

ProofGeneralの起動画面を変えることができる。

起動画面のレイアウトは、カスタマイズ変数proof-splash-contentsが持っている
ロゴ画像をカスタマイズすることもできる
URLを指定してリンク（ボタンと呼んでいいのかな？）をつくることもできる

深く探検してみたければProofGeneralのgeneric/proof-splash.elなどを読めばいいでしょう。自分のマシンのEmacsのライブラリのどこか（.../site-lisp/ProofGeneralあたり）やProofGeneralのGitHubリポジトリにあります。

起動画面をもっとカスタマイズしたい

ProofGeneralの起動画面を描画する関数は'proof-splash-insert-contentsです。
レイアウトを保持する変数が'proof-splash-contentsであることはすでに述べました。
関数'proof-splash-insert-contentsは'proof-splash-insert-contentsを参照して、起動画面のバッファにレイアウト（ロゴの描画やコピーライトの挿入など）を行います。そして起動画面の最終行に、スタートアップメッセージ'proof-splash-startup-msgを書きます。

ProofGeneralの起動画面の描画を自分で定義するために、アドバイス定義advice-addをつかって'proof-splash-insert-contentsの挙動を変更（オーバーライド）してしまうのはどうでしょうか。

(defun my/proof-splash-insert-contents ()
  (progn ; ローカルな変数を用意したければ、prognの代わりにlet*を使う 
     (setq buffer-read-only nil)
	 (erase-buffer)
	 ;;
	 ;; 画像や文字列を挿入するコードをここに書く
	 ;;
	 (goto-char (point-min))
	 (proof-splash-mode)))

(advice-add 'proof-splash-insert-contents
  :override
  #'my/proof-splash-insert-contents)

;;
;; オーバーライドを取り消すには
;; (advice-remove 'proof-splash-insert-contents #'my/proof-splash-insert-contents)
;;

'proof-splash.elのなかに「ユーザがキー入力することで、起動画面の表示を飛ばしたい、と思うはず。それを妨げるような時間のかかるプロセスはしてはならない」（意訳）というコメントがあります。時間がかかりそうな動作は非同期で行ったほうがよさそうです。もっとも自分だけで使うなら気にしなくてもいいかもしれません。

Emacsの起動画面のカスタマイズについてにでてくる具体例では、

背景画像をあらかじめ用意する
ImageMagickのconvertコマンドを呼ぶ
convertコマンドで、現在のウィンドウに合うように背景画像をリサイズ
リサイズすると同時に、用意したフォントで書いた文字列も画像に埋め込む
バッファに生成した画像を挿入する

の手順を踏んでいると思います。

おわりに

Emacsの起動画面のカスタマイズについてより引用。

fortune コマンドによる日替わり名言も追加されて、かなり意識高い画面になりました。起動画面を表示するタイミングで毎回画像を生成するため、若干起動時間が伸びますが、毎回違う画像を選ぶようにしたり、あるいはWebからネコ画像を検索してダウンロードしてくるといったようなセレンディピティな展開も可能です。もちろん非同期で画像を扱うようにすれば、急いでいるときはスキップさせるといったコードにも出来ます。

起動画面を変えることで、もっと証明をしたくなるかもしれません。たとえば、プレゼンテーション用に特別な画面を用意したり、あるいは、新年までのカウントダウンをしたりとか？

それでは、みなさま、よいクリスマスと新年をお迎えください。

この記事で用いたロゴ画像とそのライセンスについて

公式ロゴじぇねらるたんのライセンスはCC-BY-SA 3.0です。ProofGeneralのREADMEより抜粋

Proof General logo

The 2016 “chibi” icons were contributed by Yoshihiro Imai

(http://proofcafe.org/~yoshihiro503/, http://proofcafe.org/wiki/Generaltan).

They are available under the CC-BY-SA 3.0 license; for more information, see
https://creativecommons.org/licenses/by-sa/3.0/

CC-BY-SA 3.0の指示通り、本記事で用いた画像も、CC BY-SA 3.0とします。
じぇねらるたんをリサイズ、左寄せして、右にプレゼンテーションツールで適当に30分くらいで描いたツリーを置いてます。ツリーのもわもわした枝葉を描くために「雲」（説明のプレゼンなどにつかうアレ）を重ねています。