How do I make time$ work with ctrl+t e in ACL2 and emacs?

17 Views Asked by At

When trying to copy a form into my ACL2 shell buffer using ctrl+t e, and I've already placed a time$ in my shell buffer, I get an error about not being able to paste the form. How do I change the emacs macro so that I can paste into ACL2 shell buffers that already have (time$ written into them?

1

There are 1 best solutions below

0
interestedparty333 On BEST ANSWER

Place this at the end of your ~/.emacs file:

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