acl2 - 如何使 time$ 在 ACL2 和 emacs 中与 ctrl+te 一起工作？

Question

当尝试使用 ctrl+te 将表单复制到我的 ACL2 shell 缓冲区中并且我已经在 shell 缓冲区中放置了一个 time$ 时，我收到一个关于无法粘贴表单的错误。如何更改 emacs 宏，以便我可以粘贴到已经有（time$ 写入其中的 ACL2 shell 缓冲区？

Answer 1

将其放在 ~/.emacs 文件的末尾：

(setq *acl2-insert-pats* '(:not ".*%[ ]*$" "[^(]*$[ ]*$" "^$"))