/usr/share/acl2-6.5/books/tools/plev.lisp is in acl2-books-source 6.5-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 | (in-package "ACL2")
(set-state-ok t)
(defdoc plev
":Doc-Section Print-control
Easy-to-use functions for controlling the printer.~/
Example:
~bv[]
(include-book \"tools/plev\" :dir :system)
(plev) ;; moderate abbreviations, a good default
(plev-max) ;; don't abbreviate anything, show everything
(plev-min) ;; heavily abbreviate things, usually too terse
(plev-mid) ;; somewhat similar to plev
~ev[]
Each of these is actually a macro with keyword arguments
like :length, :level, :lines, :circle, :pretty, and :readably. You can choose
your own values for these arguments, or just use the above macros.
~st[Clozure Common Lisp Users]: you may wish to instead include
~bv[]
(include-book \"tools/plev-ccl\" :dir :system :ttags :all)
~ev[]
for a version of plev that also updates the print levels used during
backtraces and error messages. CCL users can also use:
~bv[]
(plev-info)
~ev[]
to see the current values of certain print-related variables.~/~/")
(link-doc-to plev-max print-control plev)
(link-doc-to plev-min print-control plev)
(link-doc-to plev-mid print-control plev)
(link-doc-to plev-info print-control plev)
(defn plev-fn (length level lines circle pretty readably state)
(declare (xargs :mode :program))
(let* ((old-tuple (abbrev-evisc-tuple state))
(new-tuple (list (car old-tuple) level length
(cadddr old-tuple))))
(mv-let (flg val state)
(set-evisc-tuple new-tuple
:iprint t
:sites :all)
(declare (ignore val))
(mv flg
(list :length length
:level level
:lines lines
:circle circle
:readably readably
:pretty pretty)
state))))
(defmacro plev (&key (length '16)
(level '3)
(lines 'nil)
(circle 't)
(pretty 't)
(readably 'nil))
`(plev-fn ,length ,level ,lines ,circle ,pretty ,readably state))
(defmacro plev-max (&key (length 'nil)
(level 'nil)
(lines 'nil)
(circle 'nil)
(pretty 't)
(readably 'nil))
`(plev-fn ,length ,level ,lines ,circle ,pretty ,readably state))
(defmacro plev-mid (&key (length '10)
(level '5)
(lines '200)
(circle 't)
(pretty 't)
(readably 'nil))
`(plev-fn ,length ,level ,lines ,circle ,pretty ,readably state))
(defmacro plev-min (&key (length '3)
(level '3)
(lines '60)
(circle 't)
(pretty 'nil)
(readably 'nil))
`(plev-fn ,length ,level ,lines ,circle ,pretty ,readably state))
|