Filtering...

base

books/xdoc/base
other
(in-package "XDOC")
other
(set-state-ok t)
other
(table xdoc 'doc nil)
other
(table xdoc 'default-parents nil)
other
(table xdoc 'post-defxdoc-event nil)
other
(table xdoc 'resource-dirs nil)
get-xdoc-tablefunction
(defun get-xdoc-table
  (world)
  (declare (xargs :mode :program))
  (cdr (assoc-eq 'doc
      (table-alist 'xdoc world))))
set-default-parentsmacro
(defmacro set-default-parents
  (&rest parents)
  `(table xdoc
    'default-parents
    (let ((parents ',XDOC::PARENTS))
      (cond ((symbol-listp parents) parents)
        ((and (consp parents)
           (atom (cdr parents))
           (symbol-listp (car parents))) (car parents))
        (t (er hard?
            'set-default-parents
            "Expected a symbol-listp, but found ~x0"
            parents))))))
get-default-parentsfunction
(defun get-default-parents
  (world)
  (declare (xargs :mode :program))
  (cdr (assoc-eq 'default-parents
      (table-alist 'xdoc world))))
check-defxdoc-argsfunction
(defun check-defxdoc-args
  (name parents short long pkg)
  (declare (xargs :guard t))
  (or (and (not (symbolp name)) "name is not a symbol!")
    (and (not (symbol-listp parents))
      ":parents are not a symbol list")
    (and short
      (not (stringp short))
      ":short is not a string (or nil)")
    (and long
      (not (stringp long))
      ":long is not a string (or nil)")
    (and pkg
      (or (not (stringp pkg))
        (equal pkg "")
        (not (pkg-witness pkg)))
      ":pkg is not a string that is a known package (or nil)")))
guard-for-defxdocfunction
(defun guard-for-defxdoc
  (name parents short long pkg)
  (declare (xargs :guard t))
  (let* ((err (check-defxdoc-args name
         parents
         short
         long
         pkg)))
    (or (not err) (cw "~s0~%" err))))
other
(local (defthm state-p1-implies-all-boundp
    (implies (state-p1 st)
      (all-boundp *initial-global-table*
        (global-table st)))
    :hints (("Goal" :in-theory (enable state-p1)))
    :rule-classes nil))
normalize-booknamefunction
(defun normalize-bookname
  (bookname)
  (declare (xargs :guard t))
  (cond ((sysfile-p bookname) (concatenate 'string
        (sysfile-filename bookname)
        " :DIR :"
        (symbol-name (sysfile-key bookname))))
    (t bookname)))
defxdoc-fnfunction
(defun defxdoc-fn
  (name parents
    short
    long
    pkg
    no-override
    state)
  (declare (xargs :mode :program :stobjs state))
  (let* ((err (check-defxdoc-args name
         parents
         short
         long
         pkg)))
    (if err
      (er hard?
        'defxdoc
        "Bad defxdoc arguments: ~s0"
        err)
      (let* ((world (w state)) (pkg (or pkg (f-get-global 'current-package state)))
          (info (f-get-global 'certify-book-info state))
          (bookname (if info
              (access certify-book-info info :full-book-name)
              "Current Interactive Session"))
          (bookname (normalize-bookname bookname))
          (parents (or parents
              (get-default-parents (w state))))
          (entry (list (cons :name name)
              (cons :base-pkg (pkg-witness pkg))
              (cons :parents parents)
              (cons :short short)
              (cons :long long)
              (cons :from bookname)))
          (table-event `(table xdoc
              'doc
              ,(IF XDOC::NO-OVERRIDE
     `(LET ((XDOC::TOPICS (XDOC::GET-XDOC-TABLE XDOC::WORLD)))
        (IF (XDOC::FIND-TOPIC ',XDOC::NAME XDOC::TOPICS)
            XDOC::TOPICS
            (CONS ',XDOC::ENTRY XDOC::TOPICS)))
     `(CONS ',XDOC::ENTRY (XDOC::GET-XDOC-TABLE XDOC::WORLD)))))
          (post-event (cdr (assoc-eq 'post-defxdoc-event
                (table-alist 'xdoc world)))))
        `(progn ,XDOC::TABLE-EVENT
          ,@(AND XDOC::POST-EVENT (LIST XDOC::POST-EVENT))
          (value-triple '(defxdoc ,XDOC::NAME)))))))
defxdocmacro
(defmacro defxdoc
  (name &key
    parents
    short
    long
    pkg
    no-override)
  `(with-output :off (event summary)
    (make-event (defxdoc-fn ',XDOC::NAME
        ',XDOC::PARENTS
        ,XDOC::SHORT
        ,XDOC::LONG
        ,XDOC::PKG
        ,XDOC::NO-OVERRIDE
        state))))
other
(table ppr-special-syms 'defxdoc 1)
defxdoc-raw-fnfunction
(defun defxdoc-raw-fn
  (name parents short long pkg)
  (declare (xargs :guard t)
    (ignore name
      parents
      short
      long
      pkg))
  (er hard?
    'defxdoc-raw-fn
    "Under-the-hood definition of defxdoc-raw-fn not installed.  You ~
       probably need to load the defxdoc-raw book."))
defxdoc-raw-after-checkfunction
(defun defxdoc-raw-after-check
  (name parents short long pkg)
  (declare (xargs :guard t))
  (let* ((err (check-defxdoc-args name
         parents
         short
         long
         pkg)))
    (if err
      (er hard?
        'defxdoc-raw
        "Bad defxdoc-raw arguments: ~s0~%"
        err)
      (defxdoc-raw-fn name
        parents
        short
        long
        pkg))))
defxdoc-rawmacro
(defmacro defxdoc-raw
  (name &key
    parents
    short
    long
    pkg)
  `(defxdoc-raw-after-check ',XDOC::NAME
    ',XDOC::PARENTS
    ,XDOC::SHORT
    ,XDOC::LONG
    ,XDOC::PKG))
find-topicfunction
(defun find-topic
  (name x)
  (declare (xargs :mode :program))
  (if (atom x)
    nil
    (if (equal (cdr (assoc :name (car x))) name)
      (car x)
      (find-topic name (cdr x)))))
gather-topic-namesfunction
(defun gather-topic-names
  (x)
  (declare (xargs :mode :program))
  (if (atom x)
    nil
    (cons (cdr (assoc :name (car x)))
      (gather-topic-names (cdr x)))))
topics-falfunction
(defun topics-fal
  (x)
  (declare (xargs :mode :program))
  (make-fast-alist (pairlis$ (gather-topic-names x) x)))