Write-strings-to-file
Write strings to a file.
;; Writes the STRINGS to 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.
(defund write-strings-to-file (strings filename ctx state)
(declare (xargs :guard (and (string-listp strings)
(stringp filename))
:stobjs state))
(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))
(if (eq channel 'acl2-output-channel::standard-character-output-0) ;todo: prove that this doesn't happen
(prog2$ (er hard? ctx "Unexpected output channel name: ~x0." channel)
(mv t state))
(pprogn (write-strings-to-channel strings channel state)
(close-output-channel channel state)
(mv nil state))))))
