[acl2/acl2] fcefd8: Incorporated further emacs/emacs-acl2.el improveme...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: fcefd87949a5e4bd00965ec8cc45a5d12177c61d
https://github.com/acl2/acl2/commit/fcefd87949a5e4bd00965ec8cc45a5d12177c61d
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2016-11-12 (Sat, 12 Nov 2016)

Changed paths:
M books/std/util/define.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M emacs/emacs-acl2.el

Log Message:
-----------
Incorporated further emacs/emacs-acl2.el improvements put forward by Keshav Kini. Fixed :T-PROOF option in DEFINE.

Quoting :doc note-7-3:

Incorporated changes to emacs/emacs-acl2.el put forward by Keshav
Kini (thanks!), as follows.

* Now, meta-x new-shell avoids buffer names that already exist.
* An error occurs when attempting to switch to a non-existent ACL2
shell buffer, rather than creating such a buffer with no
process.
* For a new shell, call shell instead of make-comint.
* Did a bit of refactoring and improved some error messages.

Thanks to Mark Greenstreet for reporting a bug in the :T-PROOF option
of DEFINE. I fixed it by taking advantage of the
MAKE-TERMINATION-THEOREM utility.

[GitHub]

Branch: refs/heads/testing