str

(in-package "XDOC")

(include-book "std/util/bstar" :dir :system)

(include-book "std/strings/printtree" :dir :system)

(local (include-book "std/util/defredundant" :dir :system))

(local (include-book "make-event/acl2x-help" :dir :system))

(program)

(make-event (b* ((state (f-put-global 'port-file-enabled-original-value
         (f-get-global 'port-file-enabled state)
         state)) (state (f-put-global 'port-file-enabled nil state)))
    (value '(:or (progn (acl2x-replace (include-book "std/strings/cat" :dir :system :uncertified-okp :ignore-certs)
            (value-triple :invisible)
            :outside-certification (include-book "std/strings/cat" :dir :system :uncertified-okp :ignore-certs))
          (acl2x-replace (include-book "std/strings/case-conversion" :dir :system :uncertified-okp :ignore-certs)
            (value-triple :invisible)
            :outside-certification (include-book "std/strings/case-conversion" :dir :system :uncertified-okp :ignore-certs))
          (acl2x-replace (include-book "std/strings/strsubst" :dir :system :uncertified-okp :ignore-certs)
            (value-triple :invisible)
            :outside-certification (include-book "std/strings/strsubst" :dir :system :uncertified-okp :ignore-certs))
          (acl2x-replace (include-book "std/strings/decimal" :dir :system :uncertified-okp :ignore-certs)
            (value-triple :invisible)
            :outside-certification (include-book "std/strings/decimal" :dir :system :uncertified-okp :ignore-certs)))
        (make-event (er hard?
            'xdoc/str
            "~%************************** XDOC/STR FAILURE **************************~%~
         Failed to include the required books.  It may be that something has ~
         changed in one of the books included here that makes it ~
         impossible to include uncertified.  Please check this by running ~
         "make clean" followed by "make xdoc/str.cert".~%~
           ************************************************************************"))))))

(make-event (b* ((state (f-put-global 'port-file-enabled
         (f-get-global 'port-file-enabled-original-value
           state)
         state)))
    (value '(value-triple :port-file-enabled-restored))))

(program)

(make-event '(:or (make-event (b* ((events (defredundant-fn '(cat implode
               implode$inline
               explode
               explode$inline
               fast-concatenate
               revappend-chars-aux
               revappend-chars
               revappend-chars$inline
               little-a
               little-z
               big-a
               big-z
               down-alpha-p
               down-alpha-p$inline
               up-alpha-p
               up-alpha-p$inline
               charlist-has-some-up-alpha-p
               charlist-has-some-down-alpha-p
               string-has-some-down-alpha-p
               string-has-some-up-alpha-p
               case-delta
               downcase-char
               downcase-char$inline
               downcase-charlist-aux
               downcase-charlist
               downcase-string-aux
               downcase-string
               upcase-char
               upcase-char$inline
               upcase-charlist-aux
               upcase-charlist
               upcase-string-aux
               upcase-string
               strprefixp-impl
               strsubst-aux
               strsubst
               make-upcase-first-strtbl
               *upcase-first-strtbl*
               upcase-first-charlist
               upcase-char-str$inline
               upcase-char-str
               upcase-first
               join-aux
               join
               join$inline
               basic-nat-to-dec-chars
               nat-to-dec-chars-aux
               nat-to-dec-chars
               nat-to-dec-chars$inline
               nat-to-dec-string
               nat-to-dec-string$inline)
             t
             state)))
        (value events)))
    (make-event (er hard?
        'xdoc/str
        "~%************************** XDOC/STR FAILURE **************************~%~
         Failed to redundantly define the required events.  If you haven't ~
         done anything to break files that this book depends on, this may be ~
         a symptom that make-event expansions from stale certificates are ~
         being loaded.  The simplest way to fix this is to run "make ~
         clean".  Otherwise, you can try to locate and delete the ~
         certificate containing the bad expansion, but you're on your own for ~
         that.~%~
           ************************************************************************"))))

(defun simple-html-encode-chars
  (x acc)
  (b* (((when (atom x)) acc) (acc (case (car x)
          (#\< (list* #\; #\t #\l #\& acc))
          (#\> (list* #\; #\t #\g #\& acc))
          (#\& (list* #\; #\p #\m #\a #\& acc))
          (#\" (list* #\; #\t #\o #\u #\q #\& acc))
          (t (cons (car x) acc)))))
    (simple-html-encode-chars (cdr x) acc)))

(defun simple-html-encode-str
  (x n xl acc)
  (b* (((when (int= n xl)) acc) (char1 (char x n))
      (acc (case char1
          (#\< (list* #\; #\t #\l #\& acc))
          (#\> (list* #\; #\t #\g #\& acc))
          (#\& (list* #\; #\p #\m #\a #\& acc))
          (#\" (list* #\; #\t #\o #\u #\q #\& acc))
          (t (cons char1 acc)))))
    (simple-html-encode-str x
      (+ 1 n)
      xl
      acc)))