[acl2/acl2] 03477e: Improved #., both its error message and by clearin...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 03477ed7b23201a9ce9b321edf014e19efbaf6b0
https://github.com/acl2/acl2/commit/03477ed7b23201a9ce9b321edf014e19efbaf6b0
Author: Matt Kaufmann <kauf...@Matts-MBP.attlocal.net>
Date: 2016-09-25 (Sun, 25 Sep 2016)

Changed paths:
M acl2-fns.lisp
M books/system/doc/acl2-doc.lisp
M books/system/doc/render-doc-base.lisp
M books/xdoc/display.lisp
M defthm.lisp
M doc.lisp
M other-events.lisp

Log Message:
-----------
Improved #., both its error message and by clearing input. Fixed error message for :definition rule with empty clique. Fixed handling of xdoc <stv> tags in text-based display. Fixed error message for bad argument of set-iprint. Improved :doc irrelevant-formals.

Quoting :doc note-7-3:

We improved ACL2's implementation of the #. read macro so that it no
longer prints additional errors after the first. Also, the error
message now mentions :DOC [sharp-dot-reader], pointing in
particular to a relevant remark when the failure occurs during book
certification.

For a proposed [definition] rule with a missing (or empty) :CLIQUE
but a non-empty :CONTROLLER-ALIST, the error message was
ill-formed. This has been fixed.

Also quoting :doc note-7-3, where this is a new item under the item,
"The text-based display of [documentation] has been improved...."

* Text within ``<stv> ... </stv>'' is now replaced by the text ``{STV
display}''. A general mechanism is in place for extending this
behavior to other tags (see xdoc-tag-elide-alist in
[community-books] file 'books/xdoc/display.lisp').

Fixed an error message in the case that the first argument of
set-iprint was not one of the supported values. (This bug was
introduced after Version 7.2.)

Improved :doc irrelevant-formals. (This is independent of the
possible change of "irrelevant" to "irrelevant-ok" in declare forms,
perhaps coming soon.)

[GitHub]

Branch: refs/heads/testing