Disable-ubt
Make it illegal to undo back through the current command
The utility disable-ubt is probably only relevant to those who
write ACL2-based tools, in particular using wormholes. Its initial
application (and perhaps still its only application) is to arrange that
insider the break-rewrite interactive loop, it is impossible to undo
the ld-keyword-aliases supporting the brr-commands.
General Forms:
:disable-ubt
(disable-ubt) ; same as above
(disable-ubt arg) ; same as above if arg is not nil or :disable-ubt
where arg is evaluated, and if it is supplied and its value is neither
nil nor :disable-ubt, then its value satisfies msgp. In
that case, the message is printed after the usual message (except, before
``See :DOC disable-ubt''). The following example illustrates the use of that
optional message but, what is more important, it illustrates the effect of
disable-ubt: a command that executes it cannot be undone.
ACL2 !>(disable-ubt (list "Just a demo: ~x0." (cons #0 17)))
Summary
Form: ( DISABLE-UBT ...)
Rules: NIL
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:DISABLE-UBT
ACL2 !>:ubt :x
ACL2 Error in :UBT: Can't undo a :disable-ubt event (at command 1).
Just a demo: 17. See :DOC disable-ubt.
ACL2 !>
Disable-ubt is similar to (reset-prehistory t), as both establish
a barrier to undoing. However, for history commands such as :pcb, command numbers are not changed by disable-ubt. Like reset-prehistory, disable-ubt is never redundant.
