diff options
| author | David Aspinall | 2010-08-03 13:20:12 +0000 |
|---|---|---|
| committer | David Aspinall | 2010-08-03 13:20:12 +0000 |
| commit | 9f8a026e13f358bb5565f21afe23f449c801d259 (patch) | |
| tree | 185a57501ea4eac2f1d58fc7b94be2d698a37d9b /generic/proof-menu.el | |
| parent | 83aa24689e8d1e933e4db35b30811d2e7062dddc (diff) | |
Add support for basic "movie" recording. See http://mws.cs.ru.nl/proviola.
Diffstat (limited to 'generic/proof-menu.el')
| -rw-r--r-- | generic/proof-menu.el | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 9efe56aa..0d671db5 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -573,8 +573,13 @@ without adjusting window layout." (defconst proof-advanced-menu (cons "Advanced" (append - '(["Complete Identifier" proof-script-complete t] - ["Insert Last Output" pg-insert-last-output-as-comment proof-shell-last-output]) + '(["Complete Identifier" proof-script-complete + :help "Complete the identifier at point"] + ["Insert Last Output" pg-insert-last-output-as-comment + :active proof-shell-last-output + :help "Insert the last output into the proof script as a comment"] + ["Make Movie" pg-movie-export + :help "Export processed portion as Movie XML file (enable Full Annotations first!)"]) (list "-----") proof-show-hide-menu (list "-----") |