• Top
  • Documentation
    • Xdoc
      • Undocumented
      • Save
      • Defsection
      • Markup
      • Preprocessor
      • Terminal
      • Emacs-links
      • Defxdoc
      • Katex-integration
      • Constructors
      • Entities
      • Save-rendered
      • Defxdoc+
      • Add-resource-directory
      • Testing
      • Order-subtopics
      • Save-rendered-event
      • Archive-matching-topics
      • Archive-xdoc
      • Xdoc-extend
      • Set-default-parents
      • Missing-parents
      • Defpointer
      • Defxdoc-raw
      • Xdoc-tests
      • Xdoc-prepend
      • Defsection-progn
      • Gen-xdoc-for-file
    • ACL2-doc
    • Recursion-and-induction
    • Loop$-primer
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Xdoc
• Defxdoc

Defxdoc+

defxdoc+ extends defxdoc with some conveniences.

In addition to the arguments of defxdoc, defxdoc+ takes the following keyword arguments:

• :order-subtopics, which must be t or nil or a non-empty list of symbols. If it is t, a call (xdoc::order-subtopics t) is generated. If it is a non-empty list (sym1 ... symN) of symbols whose last element is not t, a call (xdoc::order-subtopics (sym1 ... symN)) is generated. If it is a non-empty list of symbols (sym1 ... symN t) whose last element is t, a call (xdoc::order-subtopics (sym1 ... symN) t) is generated. If it is nil (the default), no call of xdoc::order-subtopics is generated. See xdoc::order-subtopics for a description of what the generated calls do.
• :default-parent, which must be t or nil. If it is t, a book-local call of set-default-parents is generated to use the singleton list of this topic as default parents. The default is nil.

Macro: defxdoc+

(defmacro defxdoc+ (&rest args)
 (b*
  ((name (car args))
   (keyargs (cdr args))
   ((unless (keyword-value-listp keyargs))
    (cons
     'with-output
     (cons
      ':gag-mode
      (cons
       'nil
       (cons
        ':off
        (cons
         ':all
         (cons
          ':on
          (cons
           'error
           (cons
            (cons
             'make-event
             (cons
              (cons
               'er
               (cons
                 'soft
                 (cons ''defxdoc+
                       (cons '"Malformed keyed options: ~x0"
                             (cons (cons 'quote (cons keyargs 'nil))
                                   'nil)))))
              '(:on-behalf-of :quiet!)))
            'nil)))))))))
   (must-be-nil (set-difference-eq
                     (evens keyargs)
                     '(:parents :short :long
                                :pkg :no-override
                                :order-subtopics :default-parent)))
   ((when must-be-nil)
    (cons
     'with-output
     (cons
      ':gag-mode
      (cons
       'nil
       (cons
        ':off
        (cons
         ':all
         (cons
          ':on
          (cons
           'error
           (cons
            (cons
             'make-event
             (cons
              (cons
               'er
               (cons
                'soft
                (cons
                   ''defxdoc+
                   (cons '"Unrecognized keyed option(s): ~x0"
                         (cons (cons 'quote (cons must-be-nil 'nil))
                               'nil)))))
              '(:on-behalf-of :quiet!)))
            'nil)))))))))
   (parents (cadr (assoc-keyword :parents keyargs)))
   (short (cadr (assoc-keyword :short keyargs)))
   (long (cadr (assoc-keyword :long keyargs)))
   (pkg (cadr (assoc-keyword :pkg keyargs)))
   (no-override (cadr (assoc-keyword :no-override keyargs)))
   (order-subtopics (cadr (assoc-keyword :order-subtopics keyargs)))
   (default-parent (cadr (assoc-keyword :default-parent keyargs)))
   ((unless (or (eq order-subtopics t)
                (symbol-listp order-subtopics)))
    (cons
     'with-output
     (cons
      ':gag-mode
      (cons
       'nil
       (cons
        ':off
        (cons
         ':all
         (cons
          ':on
          (cons
           'error
           (cons
            (cons
             'make-event
             (cons
              (cons
               'er
               (cons
                'soft
                (cons ''defxdoc+
                      (cons '"Malformed :ORDER-SUBTOPICS input: ~x0"
                            (cons (cons 'quote
                                        (cons order-subtopics 'nil))
                                  'nil)))))
              '(:on-behalf-of :quiet!)))
            'nil))))))))))
  (cons
   'progn
   (cons
    (cons
     'defxdoc
     (cons
      name
      (cons
       ':parents
       (cons
        parents
        (cons
         ':short
         (cons
          short
          (cons
           ':long
           (cons
                long
                (cons ':pkg
                      (cons pkg
                            (cons ':no-override
                                  (cons no-override 'nil))))))))))))
    (append
     (cond ((eq order-subtopics t)
            (cons (cons 'xdoc::order-subtopics
                        (cons name '(nil t)))
                  'nil))
           ((eq order-subtopics nil) nil)
           ((eq (car (last order-subtopics)) t)
            (cons (cons 'xdoc::order-subtopics
                        (cons name
                              (cons (butlast order-subtopics 1)
                                    '(t))))
                  'nil))
           (t (cons (cons 'xdoc::order-subtopics
                          (cons name (cons order-subtopics '(nil))))
                    'nil)))
     (and default-parent
          (cons (cons 'local
                      (cons (cons 'set-default-parents
                                  (cons name 'nil))
                            'nil))
                'nil)))))))