defxdoc-plus

(in-package "ACL2")

(defsection defxdoc+
  :parents (xdoc defxdoc)
  :short "@('defxdoc+') extends @(tsee defxdoc) with some conveniences."
  :long (topstring (p "In addition to the arguments of @(tsee defxdoc),
     @('defxdoc+') takes the following keyword arguments:")
    (ul (li "@(':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 @(tsee xdoc::order-subtopics) is generated.
      See @(tsee xdoc::order-subtopics) for
      a description of what the generated calls do.")
      (li "@(':default-parent'), which must be @('t') or @('nil').
      If it is @('t'),
      a book-@(see local) call of @(tsee set-default-parents) is generated
      to use the singleton list of this topic as default parents.
      The default is @('nil')."))
    (@def "defxdoc+"))
  (defmacro defxdoc+
    (&rest args)
    (b* ((name (car args)) (keyargs (cdr args))
        ((unless (keyword-value-listp keyargs)) `(with-output :gag-mode nil
            :off :all :on error
            (make-event (er soft 'defxdoc+ "Malformed keyed options: ~x0" ',KEYARGS)
              :on-behalf-of :quiet!)))
        (must-be-nil (set-difference-eq (evens keyargs)
            '(:parents :short :long :pkg :no-override :order-subtopics :default-parent)))
        ((when must-be-nil) `(with-output :gag-mode nil
            :off :all :on error
            (make-event (er soft
                'defxdoc+
                "Unrecognized keyed option(s): ~x0"
                ',MUST-BE-NIL)
              :on-behalf-of :quiet!)))
        (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))) `(with-output :gag-mode nil
            :off :all :on error
            (make-event (er soft
                'defxdoc+
                "Malformed :ORDER-SUBTOPICS input: ~x0"
                ',ORDER-SUBTOPICS)
              :on-behalf-of :quiet!))))
      `(progn (defxdoc ,NAME
          :parents ,PARENTS
          :short ,SHORT
          :long ,LONG
          :pkg ,PKG
          :no-override ,NO-OVERRIDE)
        ,@(COND ((EQ ORDER-SUBTOPICS T) `((XDOC::ORDER-SUBTOPICS ,NAME NIL T)))
        ((EQ ORDER-SUBTOPICS NIL) NIL)
        ((EQ (CAR (LAST ORDER-SUBTOPICS)) T)
         `((XDOC::ORDER-SUBTOPICS ,NAME ,(BUTLAST ORDER-SUBTOPICS 1) T)))
        (T `((XDOC::ORDER-SUBTOPICS ,NAME ,ORDER-SUBTOPICS NIL))))
        ,@(AND DEFAULT-PARENT `((LOCAL (SET-DEFAULT-PARENTS ,NAME)))))))
  (table ppr-special-syms 'defxdoc+ 1))