top

(defun bootstrap-revappend-chars-aux
  (x n xl y)
  (declare (xargs :mode :program)
    (type string x)
    (type (integer 0 *) n xl))
  (if (eql n xl)
    y
    (bootstrap-revappend-chars-aux x
      (the (integer 0 *) (+ 1 (the (integer 0 *) n)))
      xl
      (cons (char x n) y))))

(defun bootstrap-revappend-chars
  (x acc)
  (declare (xargs :mode :program)
    (type string x))
  (bootstrap-revappend-chars-aux x
    0
    (length x)
    acc))

(defun revappend-bar-escape-string
  (x n xl acc)
  (declare (xargs :mode :program)
    (type string x)
    (type unsigned-byte n xl))
  (if (eql n xl)
    acc
    (let* ((char (char x n)) (acc (if (or (eql char #\|) (eql char #\\))
            (cons #\\ acc)
            acc)))
      (revappend-bar-escape-string x
        (+ n 1)
        xl
        (cons char acc)))))

(defun revappend-full-escape-symbol
  (x acc)
  (declare (xargs :mode :program))
  (let* ((pkg (symbol-package-name x)) (name (symbol-name x))
      (acc (cons #\| acc))
      (acc (revappend-bar-escape-string pkg
          0
          (length pkg)
          acc))
      (acc (list* #\| #\: #\: #\| acc))
      (acc (revappend-bar-escape-string name
          0
          (length name)
          acc))
      (acc (cons #\| acc)))
    acc))

(defun colon-xdoc-initialized
  (state)
  (declare (xargs :stobjs state :mode :program))
  (cdr (assoc 'colon-xdoc-support-loaded
      (table-alist 'xdoc (w state)))))

(defun remove1-name
  (name l)
  (declare (xargs :mode :program))
  (cond ((endp l) nil)
    ((equal (cdr (assoc-eq :name (car l)))
       name) (cdr l))
    (t (cons (car l)
        (remove1-name name (cdr l))))))

(defun xdoc-extend-fn
  (name long world)
  (declare (xargs :mode :program))
  (let* ((all-topics (get-xdoc-table world)) (old-topic (find-topic name all-topics))
      (long (cond ((not long) "")
          ((stringp long) long)
          (t (er hard?
              'xdoc-extend
              "Can't extend ~x0 with non-string ~x1."
              name
              long)))))
    (cond ((not old-topic) (prog2$ (er hard?
            'xdoc-extend
            "Topic ~x0 wasn't found."
            name)
          all-topics))
      (t (let* ((other-topics (remove1-name name all-topics)) (old-long (or (cdr (assoc :long old-topic)) ""))
            (new-long (concatenate 'string old-long long))
            (new-topic (acons :long new-long
                (remove1-assoc :long old-topic))))
          (cons new-topic other-topics))))))

(defun xdoc-prepend-fn
  (name long world)
  (declare (xargs :mode :program))
  (let* ((all-topics (get-xdoc-table world)) (old-topic (find-topic name all-topics))
      (long (cond ((not long) "")
          ((stringp long) long)
          (t (er hard?
              'xdoc-extend
              "Can't prepend ~x0 with non-string ~x1."
              name
              long)))))
    (cond ((not old-topic) (er hard?
          'xdoc-prepend
          "Topic ~x0 wasn't found."
          name))
      (t (let* ((other-topics (remove1-name name all-topics)) (old-long (or (cdr (assoc :long old-topic)) ""))
            (new-long (concatenate 'string long old-long))
            (new-topic (acons :long new-long
                (remove1-assoc :long old-topic))))
          (cons new-topic other-topics))))))

(defun order-subtopics-fn
  (name order flg world)
  (declare (xargs :mode :program))
  (let* ((all-topics (get-xdoc-table world)) (old-topic (find-topic name all-topics))
      (ctx 'order-subtopics))
    (cond ((not old-topic) (er hard?
          ctx
          "Topic ~x0 wasn't found."
          name))
      ((not (symbol-listp (fix-true-list order))) (er hard?
          ctx
          "Subtopics list contains a non-symbol: ~x0"
          order))
      ((not (booleanp flg)) (er hard?
          ctx
          "Optional argument is not Boolean: ~x0"
          flg))
      (t (let* ((other-topics (remove1-name name all-topics)) (new-topic (acons :suborder (if flg
                  (append order flg)
                  order)
                (remove1-assoc :suborder old-topic))))
          (cons new-topic other-topics))))))

(defun formula-info-to-defs1
  (entries acc)
  (declare (xargs :mode :program))
  (cond ((atom entries) acc)
    ((and (consp (car entries))
       (symbolp (caar entries))) (let* ((acc (list* #\  #\? #\f #\e #\d #\( #\@ acc)) (acc (revappend-full-escape-symbol (caar entries)
              acc))
          (acc (list* #\
 #\) acc)))
        (formula-info-to-defs1 (cdr entries) acc)))
    ((stringp (car entries)) (let* ((acc (bootstrap-revappend-chars (car entries)
             acc)))
        (formula-info-to-defs1 (cdr entries) acc)))
    (t (formula-info-to-defs1 (cdr entries) acc))))

(defun formula-info-to-defs
  (headerp entries acc)
  (declare (xargs :mode :program))
  (let* ((original acc) (acc (if headerp
          (bootstrap-revappend-chars "<h3>Definitions and Theorems</h3>"
            acc)
          acc))
      (before-entries acc)
      (acc (formula-info-to-defs1 entries acc)))
    (if (equal acc before-entries)
      original
      acc)))

(defun defsection-autodoc-fn
  (name parents
    short
    long
    pkg
    extension
    marker
    state)
  (declare (xargs :mode :program :stobjs state))
  (let ((err (check-defxdoc-args name
         parents
         short
         long
         pkg)))
    (if err
      (er hard?
        'defsection
        "In section ~x0: Bad defsection arguments: ~s1~%"
        name
        err)
      (let* ((wrld (w state)) (trips (reversed-world-since-event wrld marker nil))
          (info (reverse (new-formula-info trips wrld nil)))
          (acc nil)
          (acc (if long
              (bootstrap-revappend-chars long acc)
              acc))
          (acc (list* #\
 #\
 acc))
          (acc (formula-info-to-defs (not extension)
              info
              acc))
          (long (reverse (the string (coerce acc 'string)))))
        (if extension
          `(xdoc-extend ,XDOC::EXTENSION ,XDOC::LONG)
          `(defxdoc ,XDOC::NAME
            :parents ,XDOC::PARENTS
            :short ,XDOC::SHORT
            :long ,XDOC::LONG
            :pkg ,XDOC::PKG))))))

(defun make-xdoc-fragments
  (args)
  (cond ((atom args) nil)
    ((stringp (car args)) (cons `(acl2-xdoc-fragment ,(CAR XDOC::ARGS))
        (make-xdoc-fragments (cdr args))))
    (t (cons (car args)
        (make-xdoc-fragments (cdr args))))))

(defun defsection-fn
  (wrapper name args)
  (declare (xargs :mode :program))
  (let* ((parents (cdr (extract-keyword-from-args :parents args))) (short (cdr (extract-keyword-from-args :short args)))
      (long (cdr (extract-keyword-from-args :long args)))
      (extension (cdr (extract-keyword-from-args :extension args)))
      (pkg (cdr (extract-keyword-from-args :pkg args)))
      (no-xdoc-override (cdr (extract-keyword-from-args :no-xdoc-override args)))
      (set-as-default-parent (cdr (extract-keyword-from-args :set-as-default-parent args)))
      (extension (cond ((symbolp extension) extension)
          ((and (consp extension)
             (atom (cdr extension))
             (symbolp (car extension))) (car extension))
          (t (er hard?
              'defsection
              "In section ~x0, invalid :extension: ~x1."
              name
              extension))))
      (defxdoc-p (and (not extension)
          (or parents short long)))
      (autodoc-arg (extract-keyword-from-args :autodoc args))
      (autodoc-p (and (or defxdoc-p extension)
          (or (not autodoc-arg) (cdr autodoc-arg))))
      (new-args (make-xdoc-fragments (throw-away-keyword-parts args)))
      (stack-pop-if-nonempty (if new-args
          '(:stack :pop)
          nil))
      (new-args (if set-as-default-parent
          (progn$ (and (not (equal (car wrapper) 'encapsulate))
              (er hard?
                'defsection
                "In section  ~x0, set-as-default-parent ~
                     cannot be  set to  t when the  wrapper is  not encapsulate."
                name))
            (cons `(local (set-default-parents ,XDOC::NAME))
              new-args))
          new-args))
      (wrapper (if new-args
          wrapper
          '(progn))))
    (cond ((or (not name) (not (symbolp name))) (er hard?
          'defsection
          "Section name must be a non-nil symbol; found ~
                                  ~x0."
          name))
      ((and extension (or parents short)) (er hard?
          'defsection
          "In section ~x0, you are using :extension, ~
                                  so :parents and :short are not allowed."
          name))
      ((and extension (not autodoc-p)) (er hard?
          'defsection
          "In section ~x0, you are using :extension, ~
                                  so :autodoc nil is not allowed."
          name))
      ((not autodoc-p) `(with-output :stack :push :off :all (progn ,@(AND XDOC::DEFXDOC-P
       `((XDOC::DEFXDOC ,XDOC::NAME :PARENTS ,XDOC::PARENTS :SHORT ,XDOC::SHORT
          :LONG ,XDOC::LONG :NO-OVERRIDE ,XDOC::NO-XDOC-OVERRIDE)))
            (with-output ,@XDOC::STACK-POP-IF-NONEMPTY
              (,@XDOC::WRAPPER . ,XDOC::NEW-ARGS))
            ,@(AND XDOC::EXTENSION `(XDOC::XDOC-EXTEND ,XDOC::EXTENSION ,XDOC::LONG)))))
      (t (let ((marker `(table intro-table :mark ',XDOC::NAME)))
          `(with-output :stack :push :off (:other-than error)
            (progn (table intro-table :mark nil)
              ,XDOC::MARKER
              (with-output ,@XDOC::STACK-POP-IF-NONEMPTY
                (,@XDOC::WRAPPER . ,XDOC::NEW-ARGS))
              (make-event (defsection-autodoc-fn ',XDOC::NAME
                  ',XDOC::PARENTS
                  ,XDOC::SHORT
                  ,XDOC::LONG
                  ,XDOC::PKG
                  ',XDOC::EXTENSION
                  ',XDOC::MARKER
                  state))
              (value-triple ',XDOC::NAME))))))))

(defun add-resource-directory-fn
  (dirname fullpath world)
  (declare (xargs :guard (and (stringp dirname) (stringp fullpath))
      :mode :program))
  (let* ((resource-dirs (cdr (assoc-eq 'resource-dirs
           (table-alist 'xdoc world)))) (look (cdr (assoc-equal dirname resource-dirs))))
    (if look
      (if (equal look fullpath)
        resource-dirs
        (er hard?
          'add-resource-directory
          "Conflicting paths for resource directory ~x0.~%  ~
                 - Previous path: ~x1.~%  ~
                 - New path: ~x2."
          dirname
          look
          fullpath))
      (cons (cons dirname fullpath)
        resource-dirs))))