#! /bin/sh
# A. Flatau  9-Jul-1993; modified by M. Kaufmann, 26-Oct-1993, also 8/94 and 10/94, etc.
#

# This script should be run by executing
#   make DOC
# or
#   make TEXINFO
# from the main ACL2 directory.  The make variable PREFIX is used in this script.

rm -f doc/workxxx

# The next six non-blank lines should be commented out if we don't want to
# destroy what's in the saved/ subdirectories.

rm -f doc/EMACS/saved/*
rm -f doc/LEMACS/saved/*
# rm -f doc/TEX/saved/*

# We need to get rid of .aux file of TEX.  So, we'll let the user do his
# own saving, and otherwise delete everything.

touch doc/EMACS/temp.temp
mv -f doc/EMACS/*.* doc/EMACS/saved
touch doc/LEMACS/temp.temp
mv -f doc/LEMACS/*.* doc/LEMACS/saved

# See comment above.
# mv -f doc/TEX/*.* doc/TEX/saved

rm -f doc/TEX/*.*

# Some ACL2 images start up inside LP; some don't.  (value :q) always gets us
# out of the loop, and should also be harmless when executed in raw Lisp.
# However, note that Lispworks requires that the two forms not all be on the
# same line.

echo '(value :q)' > doc/workxxx
echo '(lp)' >> doc/workxxx

echo '(certify-book "doc/write-acl2-texinfo")' >> doc/workxxx

echo '(write-texinfo-file :dir-string "doc/EMACS/" :file "acl2-doc-emacs" :tex-only-flg nil :non-lucid-flg t)' >> doc/workxxx

echo '(write-texinfo-file :dir-string "doc/LEMACS/" :file "acl2-doc-lemacs" :tex-only-flg nil)' >> doc/workxxx

echo '(write-tex-file :dir-string "doc/TEX/" :file "acl2-book")' >> doc/workxxx

echo ':q' >> doc/workxxx

${PREFIX}saved_acl2 < doc/workxxx

emacs -batch "doc/EMACS/acl2-doc-emacs.texinfo" -l "../make-texinfo.el" -f texinfo-format-buffer-and-save

emacs -batch "doc/LEMACS/acl2-doc-lemacs.texinfo" -l "../make-texinfo.el" -f texinfo-format-buffer-and-save

cd doc/TEX

cp ../texinfo.tex .
texi2dvi acl2-book.tex

dvips acl2-book.dvi -o acl2-book.ps

# To debug bad documentation:
# Start up ACL2 in the source directory.
# (include-book "doc/write-acl2-texinfo")
# Apply DEFDOC to fix bad documentation.
# (write-texinfo-file :dir-string "doc/EMACS/" :file "acl2-doc-emacs" :tex-only-flg nil :non-lucid-flg t)
# One can write others too:
#
# (write-texinfo-file :dir-string "doc/LEMACS/" :file "acl2-doc-lemacs" :tex-only-flg nil)
# (write-tex-file :dir-string "doc/TEX/" :file "acl2-book")