Write-strings-to-file!
Write strings to a file when not allowed without a trust tag.
;; Writes the STRINGS to file FILENAME, overwriting its previous contents.
;; Effectively, all the STRINGS get concatenated and the result becomes the new
;; contents of the file. Returns (mv erp state). CTX is a context for error
;; printing. The ttag is needed because this calls open-output-channel!, but
;; that makes this version usable during make-event expansion,
;; clause-processors, etc.
(defund write-strings-to-file! (strings filename ctx state)
(declare (xargs :stobjs state
:guard (and (string-listp strings)
(stringp filename))))
(mv-let (channel state)
(open-output-channel! filename :character state)
(if (not channel)
(prog2$ (er hard? ctx "Unable to open file ~s0 for :character output." filename)
(mv t state))
(pprogn (write-strings-to-channel strings channel state)
(close-output-channel channel state)
(mv nil state)))))
