misc cleanup -- no need to copy style files;
authorwenzelm
Sun May 01 16:52:29 2011 +0200 (2011-05-01)
changeset 42512f1ca2b0e0265
parent 42511 bf89455ccf9d
child 42513 96a55556639c
misc cleanup -- no need to copy style files;
doc-src/TutorialI/IsaMakefile
doc-src/ZF/IsaMakefile
     1.1 --- a/doc-src/TutorialI/IsaMakefile	Sun May 01 16:36:34 2011 +0200
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Sun May 01 16:52:29 2011 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Fun \
     1.6    HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Types HOL-Misc \
     1.7 -  HOL-Protocol HOL-Documents styles
     1.8 +  HOL-Protocol HOL-Documents
     1.9  images:
    1.10  test:
    1.11  all: default
    1.12 @@ -26,17 +26,6 @@
    1.13  HOL:
    1.14  	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
    1.15  
    1.16 -styles:
    1.17 -	@rm -f isabelle.sty
    1.18 -	@rm -f isabellesym.sty
    1.19 -	@rm -f pdfsetup.sty
    1.20 -	@$(ISABELLE_TOOL) latex -o sty >/dev/null
    1.21 -	@rm -f pdfsetup.sty
    1.22 -	@rm -f */document/isabelle.sty
    1.23 -	@rm -f */document/isabellesym.sty
    1.24 -	@rm -f */document/pdfsetup.sty
    1.25 -	@rm -f */document/session.tex
    1.26 -
    1.27  
    1.28  
    1.29  ## HOL-Ifexpr
    1.30 @@ -45,6 +34,10 @@
    1.31  
    1.32  $(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
    1.33  	$(USEDIR) Ifexpr
    1.34 +	@rm -f Ifexpr/document/isabelle.sty
    1.35 +	@rm -f Ifexpr/document/isabellesym.sty
    1.36 +	@rm -f Ifexpr/document/pdfsetup.sty
    1.37 +	@rm -f Ifexpr/document/session.tex
    1.38  	@rm -f tutorial.dvi
    1.39  
    1.40  ## HOL-ToyList
    1.41 @@ -56,10 +49,18 @@
    1.42  
    1.43  $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML
    1.44  	$(USEDIR) ToyList2
    1.45 +	@rm -f ToyList2/document/isabelle.sty
    1.46 +	@rm -f ToyList2/document/isabellesym.sty
    1.47 +	@rm -f ToyList2/document/pdfsetup.sty
    1.48 +	@rm -f ToyList2/document/session.tex
    1.49  	@rm -f tutorial.dvi
    1.50  
    1.51  $(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML
    1.52  	$(USEDIR) ToyList
    1.53 +	@rm -f ToyList/document/isabelle.sty
    1.54 +	@rm -f ToyList/document/isabellesym.sty
    1.55 +	@rm -f ToyList/document/pdfsetup.sty
    1.56 +	@rm -f ToyList/document/session.tex
    1.57  	@rm -f tutorial.dvi
    1.58  
    1.59  ## HOL-CodeGen
    1.60 @@ -68,6 +69,10 @@
    1.61  
    1.62  $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy
    1.63  	$(USEDIR) CodeGen
    1.64 +	@rm -f CodeGen/document/isabelle.sty
    1.65 +	@rm -f CodeGen/document/isabellesym.sty
    1.66 +	@rm -f CodeGen/document/pdfsetup.sty
    1.67 +	@rm -f CodeGen/document/session.tex
    1.68  	@rm -f tutorial.dvi
    1.69  
    1.70  
    1.71 @@ -79,6 +84,10 @@
    1.72    Datatype/Nested.thy Datatype/unfoldnested.thy \
    1.73    Datatype/Fundata.thy
    1.74  	$(USEDIR) Datatype
    1.75 +	@rm -f Datatype/document/isabelle.sty
    1.76 +	@rm -f Datatype/document/isabellesym.sty
    1.77 +	@rm -f Datatype/document/pdfsetup.sty
    1.78 +	@rm -f Datatype/document/session.tex
    1.79  	@rm -f tutorial.dvi
    1.80  
    1.81  
    1.82 @@ -88,6 +97,10 @@
    1.83  
    1.84  $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy
    1.85  	$(USEDIR) Trie
    1.86 +	@rm -f Trie/document/isabelle.sty
    1.87 +	@rm -f Trie/document/isabellesym.sty
    1.88 +	@rm -f Trie/document/pdfsetup.sty
    1.89 +	@rm -f Trie/document/session.tex
    1.90  	@rm -f tutorial.dvi
    1.91  
    1.92  
    1.93 @@ -97,6 +110,10 @@
    1.94  
    1.95  $(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy
    1.96  	$(USEDIR) Fun
    1.97 +	@rm -f Fun/document/isabelle.sty
    1.98 +	@rm -f Fun/document/isabellesym.sty
    1.99 +	@rm -f Fun/document/pdfsetup.sty
   1.100 +	@rm -f Fun/document/session.tex
   1.101  	@rm -f tutorial.dvi
   1.102  
   1.103  
   1.104 @@ -106,6 +123,10 @@
   1.105  
   1.106  $(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML
   1.107  	$(USEDIR) Advanced
   1.108 +	@rm -f Advanced/document/isabelle.sty
   1.109 +	@rm -f Advanced/document/isabellesym.sty
   1.110 +	@rm -f Advanced/document/pdfsetup.sty
   1.111 +	@rm -f Advanced/document/session.tex
   1.112  	@rm -f tutorial.dvi
   1.113  
   1.114  ## HOL-Rules
   1.115 @@ -116,6 +137,10 @@
   1.116  	Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \
   1.117  	Rules/Tacticals.thy Rules/find2.thy Rules/ROOT.ML 
   1.118  	@$(USEDIR) Rules
   1.119 +	@rm -f Rules/document/isabelle.sty
   1.120 +	@rm -f Rules/document/isabellesym.sty
   1.121 +	@rm -f Rules/document/pdfsetup.sty
   1.122 +	@rm -f Rules/document/session.tex
   1.123  	@rm -f tutorial.dvi
   1.124  
   1.125  ## HOL-Sets
   1.126 @@ -125,6 +150,10 @@
   1.127  $(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \
   1.128  	Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML
   1.129  	@$(USEDIR) Sets
   1.130 +	@rm -f Sets/document/isabelle.sty
   1.131 +	@rm -f Sets/document/isabellesym.sty
   1.132 +	@rm -f Sets/document/pdfsetup.sty
   1.133 +	@rm -f Sets/document/session.tex
   1.134  	@rm -f tutorial.dvi
   1.135  
   1.136  ## HOL-CTL
   1.137 @@ -133,6 +162,10 @@
   1.138  
   1.139  $(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML
   1.140  	$(USEDIR) CTL
   1.141 +	@rm -f CTL/document/isabelle.sty
   1.142 +	@rm -f CTL/document/isabellesym.sty
   1.143 +	@rm -f CTL/document/pdfsetup.sty
   1.144 +	@rm -f CTL/document/session.tex
   1.145  	@rm -f tutorial.dvi
   1.146  
   1.147  ## HOL-Inductive
   1.148 @@ -143,6 +176,10 @@
   1.149    Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \
   1.150    Inductive/Advanced.thy
   1.151  	$(USEDIR) Inductive
   1.152 +	@rm -f Inductive/document/isabelle.sty
   1.153 +	@rm -f Inductive/document/isabellesym.sty
   1.154 +	@rm -f Inductive/document/pdfsetup.sty
   1.155 +	@rm -f Inductive/document/session.tex
   1.156  	@rm -f tutorial.dvi
   1.157  
   1.158  ## HOL-Types
   1.159 @@ -153,6 +190,10 @@
   1.160    Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \
   1.161    Types/Overloading.thy Types/Axioms.thy
   1.162  	$(USEDIR) Types
   1.163 +	@rm -f Types/document/isabelle.sty
   1.164 +	@rm -f Types/document/isabellesym.sty
   1.165 +	@rm -f Types/document/pdfsetup.sty
   1.166 +	@rm -f Types/document/session.tex
   1.167  	@rm -f tutorial.dvi
   1.168  
   1.169  ## HOL-Misc
   1.170 @@ -164,6 +205,10 @@
   1.171    Misc/Option2.thy Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
   1.172    Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
   1.173  	$(USEDIR) Misc
   1.174 +	@rm -f Misc/document/isabelle.sty
   1.175 +	@rm -f Misc/document/isabellesym.sty
   1.176 +	@rm -f Misc/document/pdfsetup.sty
   1.177 +	@rm -f Misc/document/session.tex
   1.178  	@rm -f tutorial.dvi
   1.179  
   1.180  
   1.181 @@ -175,6 +220,10 @@
   1.182    Protocol/Message.thy Protocol/Event.thy \
   1.183    Protocol/Public.thy Protocol/NS_Public.thy    
   1.184  	$(USEDIR) Protocol
   1.185 +	@rm -f Protocol/document/isabelle.sty
   1.186 +	@rm -f Protocol/document/isabellesym.sty
   1.187 +	@rm -f Protocol/document/pdfsetup.sty
   1.188 +	@rm -f Protocol/document/session.tex
   1.189  	@rm -f tutorial.dvi
   1.190  
   1.191  ## HOL-Documents
   1.192 @@ -183,6 +232,10 @@
   1.193  
   1.194  $(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML
   1.195  	$(USEDIR) Documents
   1.196 +	@rm -f Documents/document/isabelle.sty
   1.197 +	@rm -f Documents/document/isabellesym.sty
   1.198 +	@rm -f Documents/document/pdfsetup.sty
   1.199 +	@rm -f Documents/document/session.tex
   1.200  	@rm -f tutorial.dvi
   1.201  
   1.202  ## clean
     2.1 --- a/doc-src/ZF/IsaMakefile	Sun May 01 16:36:34 2011 +0200
     2.2 +++ b/doc-src/ZF/IsaMakefile	Sun May 01 16:52:29 2011 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4  
     2.5  ## targets
     2.6  
     2.7 -default: ZF-examples styles
     2.8 +default: ZF-examples
     2.9  images:
    2.10  test:
    2.11  all: default
    2.12 @@ -15,8 +15,7 @@
    2.13  SRC = $(ISABELLE_HOME)/src
    2.14  OUT = $(ISABELLE_OUTPUT)
    2.15  LOG = $(OUT)/log
    2.16 -OPTIONS = -m brackets -i true -d "" -D document
    2.17 -USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS) $(OUT)/ZF
    2.18 +USEDIR = @$(ISABELLE_TOOL) usedir -m brackets -i true -d "" -D document
    2.19  
    2.20  
    2.21  ## ZF
    2.22 @@ -24,17 +23,6 @@
    2.23  ZF:
    2.24  	@cd $(SRC)/ZF; $(ISABELLE_TOOL) make ZF
    2.25  
    2.26 -styles:
    2.27 -	@rm -f isabelle.sty
    2.28 -	@rm -f isabellesym.sty
    2.29 -	@rm -f pdfsetup.sty
    2.30 -	@$(ISABELLE_TOOL) latex -o sty >/dev/null
    2.31 -	@rm -f pdfsetup.sty
    2.32 -	@rm -f document/isabelle.sty
    2.33 -	@rm -f document/isabellesym.sty
    2.34 -	@rm -f document/pdfsetup.sty
    2.35 -	@rm -f document/session.tex
    2.36 -
    2.37  
    2.38  ## ZF-examples
    2.39  
    2.40 @@ -42,7 +30,11 @@
    2.41  
    2.42  $(LOG)/ZF-examples.gz: $(OUT)/ZF \
    2.43  	FOL_examples.thy  IFOL_examples.thy ZF_examples.thy If.thy ROOT.ML 
    2.44 -	@$(USEDIR) .
    2.45 +	@$(USEDIR) -s examples $(OUT)/ZF .
    2.46 +	@rm -f document/isabelle.sty
    2.47 +	@rm -f document/isabellesym.sty
    2.48 +	@rm -f document/pdfsetup.sty
    2.49 +	@rm -f document/session.tex
    2.50  
    2.51  ## clean
    2.52