Major Section: SWITCHES-PARAMETERS-AND-MODES
General Forms:
(set-ignore-doc-string-error nil) ; :doc strings must be well-formed
(set-ignore-doc-string-error t) ; ill-formed :doc strings are ignored
(set-ignore-doc-string-error :warn) ; ill-formed :doc strings are ignored
; except for causing a warning
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so recorded.
General Form: (set-ignore-doc-string-error flag)where
flag is nil, t, or :warn, as indicated above.
This macro is essentially equivalent to
(table acl2-defaults-table :ignore-doc-string-error flag)and hence is
local to any books and encapsulate events
in which it occurs; see acl2-defaults-table. However, unlike the above
simple call of the table event function (see table), no output results
from a set-ignore-doc-string-error event.Note that since defdoc events have the sole purpose of installing
documentation strings, these require well-formed documentation strings
even after executing a call of ignore-doc-string-error.
The default behavior of the system is as though the
:ignore-doc-string-error value is nil. The current behavior can be
ascertained by evaluating the following form.
(ignore-doc-string-error (w state))
