[acl2/acl2] b4c32d: Improved theory-invariant messages. Fixed :pe for...

[GitHub]

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

Changed paths:
M books/misc/check-acl2-exports.lisp
M books/rtl/rel11/lib/doc.lisp
M books/std/util/define.lisp
M books/system/doc/acl2-doc.lisp
M defpkgs.lisp
M doc.lisp
M emacs/acl2-doc.el
M other-events.lisp
M type-set-b.lisp

Log Message:
-----------
Improved theory-invariant messages. Fixed :pe for define to show guards and more. Added 3 symbols to *acl2-exports*. Cleaned up rtl :doc. Improved acl2-doc browser, dealing better with `:' and [n], and enhancing "i" command to count the matches.

Quoting :doc note-7-3 (the latter part of the change above (showing a
book) was J's idea):

Warning and error messages produced upon [theory-invariant]
violations now include additional explanation. Thanks to David
Hardin and Grant Passmore for helpful remarks leading us to make
this change. Those messages also now show where the theory
invariant was defined: a book pathname, or ``top-level'' if
directly in the loop.

The use of :pe on a form introduced by DEFINE now shows the guards
and, more generally, is more faithful to the actual form. Thanks to
Eric Smith for pointing out that the guard was missing.

Added the following symbols to *acl2-exports*: ER-LET*,
SET-BAD-LISP-CONSP-MEMOIZE, and WITH-GUARD-CHECKING-EVENT.

Cleaned up rtl :doc warnings and tweaked links from the rtl pages to
David Russinoff's rtl manual.

Fixed acl2-doc to deal better with names containing the `:' character.
For example, clicking on child links Rtl::MASC:_The_Formal_Language
(from RTL::MODELING_ALGORITHMS_IN_SYSTEMC_AND_ACL2) and
Gl::6._Writing_:g-bindings_forms (GL::BASIC-TUTORIAL) had failed.
That change has been mentioned by expanding an existing release note
(sub-)item, but here are two new (sub-) items (quoting :doc note-7-3):

* Text in square brackets, for example [1], is no longer recognized as
a link (though Emacs still highlights it). Thanks to Mihir
Mehta for pointing out this issue.

* In the [ACL2-doc] browser, when the ``i'' (acl2-doc-index) command is
invoked without a prefix argument, the mode line shows the
number of matches. (The remaining matches continue to be
accessible using the ``,'' (acl2-doc-index-next) command.)

[GitHub]

Branch: refs/heads/testing