diff -r c4783e4ef43f -r a04084de4946 IsaMakefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/IsaMakefile Thu Dec 06 15:12:49 2012 +0000 @@ -0,0 +1,51 @@ + +## targets + +default: itp +all: session itp slides1 + +## global settings + +SRC = $(ISABELLE_HOME)/src +OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log + + +USEDIR = $(ISABELLE_TOOL) usedir -v true -t true + + +## Slides + +session1: Slides/ROOT1.ML \ + Slides/document/root* \ + Slides/Slides1.thy + @$(USEDIR) -D generated -f ROOT1.ML HOL Slides + +slides1: session1 + rm -f Slides/generated/*.aux # otherwise latex will fall over + cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex + cp Slides/generated/root.beamer.pdf Slides/slides.pdf + +# main files + +session: ./ROOT.ML ./*.thy + @$(USEDIR) -b -D generated -f ROOT.ML HOL Prio + + +# itp paper + +itp: Paper/*.thy Paper/*.ML + @$(USEDIR) -D generated -f ROOT.ML Prio Paper + rm -f Paper/generated/*.aux # otherwise latex will fall over + cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex + cd Paper/generated ; bibtex root + cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex + cp Paper/generated/root.pdf paper.pdf + + +slides: Slides/ROOT1.ML Slides/*.thy + @$(USEDIR) -D generated -f ROOT1.ML Prio Slides + rm -f Slides/generated/*.aux # otherwise latex will fall over + cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex + cp Slides/generated/root.beamer.pdf Slides/slides.pdf +