## targets

default: slides4
all: slides itp

## global settings

SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log


USEDIR = $(ISABELLE_TOOL) usedir -v true -t true 


## Slides 1

session1: Slides/ROOT.ML \
         Slides/document/root* \
         Slides/Slides.thy
	@$(USEDIR) -D generated -f ROOT.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/slides1.pdf     

## Slides 2

session2: Slides/ROOT.ML \
         Slides/document/root* \
         Slides/Slides1.thy
	@$(USEDIR) -D generated -f ROOT1.ML HOL Slides

slides2: session2 
	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/slides2.pdf   

## Slides 3

session3: Slides/ROOT.ML \
         Slides/document/root* \
         Slides/Slides2.thy
	@$(USEDIR) -D generated -f ROOT2.ML HOL Slides

slides3: session3 
	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/slides3.pdf   

## Slides 4

session4: Slides/ROOT.ML \
         Slides/document/root* \
         Slides/Slides4.thy
	@$(USEDIR) -D generated -f ROOT4.ML HOL Slides

slides4: session4 
	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/slides4.pdf  

## Slides 5

session5: Slides/ROOT.ML \
         Slides/document/root* \
         Slides/Slides5.thy
	@$(USEDIR) -D generated -f ROOT5.ML HOL Slides

slides5: session5 
	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/slides5.pdf  



slides: slides1 slides2 slides3 slides4 slides5


## ITP itp

session_itp: Paper/ROOT.ML \
	Paper/document/root* \
	Paper/*.thy
	@$(USEDIR) -D generated -f ROOT.ML HOL Paper

itp: session_itp
	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     

## Journal Version

session_journal: Journal/ROOT.ML \
	Journal/document/root* \
	Journal/*.thy
	@$(USEDIR) -D generated -f ROOT.ML HOL Journal

journal: session_journal
	rm -f Journal/generated/*.aux # otherwise latex will fall over       
	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
	cd Journal/generated ; bibtex root
	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
	cp Journal/generated/root.pdf journal.pdf     


## clean

clean:
	rm -rf Slides/generated*
	rm -rf Paper/generated*
	rm -rf Journal/generated*