diff -r aead2aad845c -r 09bbed4f21d6 IsaMakefile --- a/IsaMakefile Mon May 24 21:11:33 2010 +0100 +++ b/IsaMakefile Tue May 25 00:24:41 2010 +0100 @@ -60,6 +60,27 @@ $(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated @cp Quotient-Paper/document.pdf qpaper.pdf +## Slides + +session1: Slides/ROOT.ML \ + Slides/document/root* \ + Slides/Slides1.thy + @$(USEDIR) -D generated1 -f ROOT.ML HOL-Nominal Slides + @perl -i -p -e "s/..isachardoublequoteopen./\\\begin{innerdouble}/g" Sl + @perl -i -p -e "s/..isachardoublequoteclose./\\\end{innerdouble}/g" Sli + @perl -i -p -e "s/..isacharbackquoteopen./\\\begin{innersingle}/g" Slid + @perl -i -p -e "s/..isacharbackquoteclose./\\\end{innersingle}/g" Slide + +slides1: session1 + rm -f Slides/generated1/*.aux # otherwise latex will fall over + cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex + cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex + cp Slides/generated1/root.beamer.pdf Slides/slides.pdf + +slides: slides1 + + + ## clean