From 1d677e46e12f4e243b89478f84b47bfdf96b3c14 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 28 Aug 2000 12:32:59 +0000 Subject: Split manual into two parts. Added notes about find theorems trick of separating constants by comma for Isabelle. Made for version 99-1. Improved documentation for urgent messages, including recent additions. Mentioned new high-level macros proof-defshortcut, proof-definvisible. --- doc/Makefile.doc | 165 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 doc/Makefile.doc (limited to 'doc/Makefile.doc') diff --git a/doc/Makefile.doc b/doc/Makefile.doc new file mode 100644 index 00000000..0ab113e1 --- /dev/null +++ b/doc/Makefile.doc @@ -0,0 +1,165 @@ +## +## Makefile for Proof General doc directory. +## +## Author: David Aspinall +## +## Maintainer: Proof General maintainer +## +## $Id$ +## +########################################################################### +## +## Use: +## make info,dvi,pdf,html - build respective docs from texi source. +## make doc - make default kinds of doc (dvi, info). +## +########################################################################### + +# DOCNAME = ProofGeneral + +MAKEINFO = makeinfo +TEXI2DVI = texi2dvi + +# `dviutils' package contains these useful utilities. +# "make rearrange" will only be called if you have dviselect. +DVISELECT = dviselect +DVICONCAT = dviconcat + + +# Assumes actual first two pages belong to titlepage +TITLERANGE = =1,=2 + +# Assumes that main document starts on third actual page +MAINRANGE = =3,=4,3: + +TOC = :_1 + +DVI2PS = dvips +TEXI2PDF = texi2pdf +TEXI2HTML = texi2html -expandinfo -number -split_chapter +# FIXME: choose emacs automatically if xemacs not available +EMACS = xemacs -batch + +TMPFILE=pgt + +.SUFFIXES: .texi .info .dvi .html .pdf .ps .eps .tiff .gz + +default: doc + +.texi.info: + $(MAKEINFO) $< + +.texi.dvi: + $(TEXI2DVI) $< + if `which $(DVISELECT) > /dev/null`; then $(MAKE) rearrange; fi + +rearrange: + $(DVISELECT) -i $(DOCNAME).dvi -o $(DOCNAME).tmp1 $(TITLERANGE) + $(DVISELECT) -i $(DOCNAME).dvi -o $(DOCNAME).tmp2 $(MAINRANGE) + $(DVISELECT) -i $(DOCNAME).dvi -o $(DOCNAME).tmp3 $(TOC) + $(DVICONCAT) -o $(DOCNAME).dvi $(DOCNAME).tmp1 $(DOCNAME).tmp3 $(DOCNAME).tmp2 + rm -f $(DOCNAME).tmp1 $(DOCNAME).tmp2 $(DOCNAME).tmp3 + +.tiff.eps: + tiff2ps -e -w 3.48 -h 5 $*.tiff > $*.eps + +## FIXME: need to do page rearrangement here, too! +.texi.pdf: + $(TEXI2PDF) $< + +.dvi.ps: + $(DVI2PS) $< -o $*.ps + +.texi.html: + $(TEXI2HTML) $< + +default: doc + +ProofGeneral.txt: + echo > ProofGeneral.txt + +# In fact, the flag seems not to work (why?), +# so comment out the image line too. +# NB! mustn't have another line with '@c image' in it. +ProofGeneralPortrait.eps: + if [ -f ProofGeneralPortrait.eps.gz ]; then gunzip -c ProofGeneralPortrait.eps.gz > ProofGeneralPortrait.eps; fi + if [ -f ProofGeneralPortrait.eps ]; then \ + sed 's/@clear haveeps/@set haveeps/g' ProofGeneral.texi > $(TMPFILE); \ + sed 's/@c image{ProofGeneralPortrait}/@image{ProofGeneralPortrait}/g' $(TMPFILE) > ProofGeneral.texi; \ + else \ + sed 's/@set haveeps/@clear haveeps/g' ProofGeneral.texi > $(TMPFILE); \ + sed 's/@image{ProofGeneralPortrait}/@c image{ProofGeneralPortrait}/g' $(TMPFILE) > ProofGeneral.texi; \ + fi + rm -f $(TMPFILE) + +ProofGeneralPortrait.pdf: + if [ -f ProofGeneralPortrait.eps.gz ]; then gunzip -c ProofGeneralPortrait.eps.gz > ProofGeneralPortrait.eps; epstopdf ProofGeneralPortrait.eps; fi + if [ -f ProofGeneralPortrait.pdf ]; then \ + sed 's/@clear haveeps/@set haveeps/g' ProofGeneral.texi > $(TMPFILE); \ + sed 's/@c image{ProofGeneralPortrait}/@image{ProofGeneralPortrait}/g' $(TMPFILE) > ProofGeneral.texi; \ + else \ + sed 's/@set haveeps/@clear haveeps/g' ProofGeneral.texi > $(TMPFILE); \ + sed 's/@image{ProofGeneralPortrait}/@c image{ProofGeneralPortrait}/g' $(TMPFILE) > ProofGeneral.texi; \ + fi + rm -f $(TMPFILE) + +%.gz : % + gzip -f -9 $* + +## +## doc : build info and dvi files from $(DOCNAME).texi +## +doc: dvi info + + +## +## all : build all documentation targets +## +all: dvi ps html info pdf + +## +## dist: build distribution targets +## +dist: info html psz pdf + +dvi: ProofGeneralPortrait.eps $(DOCNAME).dvi +ps: dvi $(DOCNAME).ps +psz: ps $(DOCNAME).ps.gz +pdf: ProofGeneralPortrait.pdf $(DOCNAME).pdf +html: $(DOCNAME).html + ln -sf $(DOCNAME)_toc.html index.html +info: ProofGeneral.txt $(DOCNAME).info + +# NB: for info, could make localdir automatically from +# START-INFO-DIR-ENTRY / END-INFO-DIR-ENTRY. +# Does some utility do this? + +## +## clean: Remove subsidiary documentation files +## +clean: + rm -f ProofGeneral.txt ProofGeneralPortrait.eps ProofGeneralPortrait.pdf + rm -f $(DOCNAME).{cp,fn,vr,tp,ky,pg} + rm -f $(DOCNAME).{fns,vrs,cps,aux,log,toc,kys,cp0} + rm -f *~ + +## +## distclean: Remove documentation targets +## +distclean: clean + rm -f $(DOCNAME).info* $(DOCNAME).dvi $(DOCNAME)*.ps $(DOCNAME).pdf $(DOCNAME)*.html + +## +## texi: update magic comments in texi from docstrings in code. +## (developer use only!) +## +$(DOCNAME).texi: ../*/*.el + $(MAKE) magic +magic: + $(EMACS) -l docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer + + + + + + -- cgit v1.2.3