• Top
    • Documentation
      • Xdoc
        • Undocumented
        • Save
        • Defsection
        • Markup
        • Preprocessor
        • Emacs-links
        • Defxdoc
        • Katex-integration
        • Constructors
        • Entities
        • Save-rendered
        • Add-resource-directory
        • Defxdoc+
          • Testing
          • Order-subtopics
          • Save-rendered-event
          • Archive-matching-topics
          • Missing-parents
          • Archive-xdoc
          • Xdoc-extend
          • Set-default-parents
          • Defpointer
          • Defxdoc-raw
          • Xdoc-tests
          • Xdoc-prepend
          • Defsection-progn
          • Gen-xdoc-for-file
        • ACL2-doc
        • Pointers
        • Doc
        • Documentation-copyright
        • Args
        • ACL2-doc-summary
        • Finding-documentation
        • Broken-link
      • Books
      • Recursion-and-induction
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • 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 of xdoc::order-subtopics is generated to order all the subtopics of this topic. If it is a non-empty list of symbols, a call of xdoc::order-subtopics is generated to order the subtopics in the list according to the list. If it is nil (the default), no call of xdoc::order-subtopics is generated.
    • :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)
               (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)))))))