Filtering...

fmt-to-str-orig

books/xdoc/fmt-to-str-orig
other
(in-package "XDOC")
other
(include-book "std/util/bstar" :dir :system)
other
(set-state-ok t)
other
(program)
fmt-to-str-orig-auxfunction
(defun fmt-to-str-orig-aux
  (string alist base-pkg state)
  (b* ((hard-right-margin (f-get-global 'fmt-hard-right-margin state)) (soft-right-margin (f-get-global 'fmt-soft-right-margin state))
      (print-case (f-get-global 'print-case state))
      (pkg (current-package state))
      (base-pkg-name (symbol-package-name base-pkg))
      ((mv er ?val state) (in-package-fn base-pkg-name state))
      ((when er) (er hard?
          'fmt-to-str-orig-aux
          "Error switching to package ~x0"
          base-pkg-name)
        (mv "" state))
      (state (set-fmt-hard-right-margin 68 state))
      (state (set-fmt-soft-right-margin 62 state))
      (state (set-print-case :downcase state))
      ((mv channel state) (open-output-channel :string :character state))
      ((mv ?col state) (fmt1 string
          alist
          0
          channel
          state
          nil))
      ((mv er1 str state) (get-output-stream-string$ channel state))
      ((mv er2 ?val state) (in-package-fn pkg state))
      (state (set-fmt-hard-right-margin hard-right-margin
          state))
      (state (set-fmt-soft-right-margin soft-right-margin
          state))
      (state (set-print-case print-case state))
      ((when er1) (er hard?
          'fmt-to-str-orig-aux
          "Error with get-output-stream-string$?")
        (mv "" state))
      ((when er2) (er hard?
          'fmt-to-str-orig-aux
          "Error switching back to package ~x0"
          pkg)
        (mv "" state)))
    (mv str state)))
fmt-to-str-origfunction
(defun fmt-to-str-orig
  (x base-pkg state)
  (fmt-to-str-orig-aux "~x0"
    (list (cons #\0 x))
    base-pkg
    state))