Admin/page/Makefile
changeset 8056 3c587e7b8fe5
child 8132 b93992e26c6a
equal deleted inserted replaced
8055:bb15396278fb 8056:3c587e7b8fe5
       
     1 # --- uses $DISTNAME environment variable 
       
     2 
       
     3 # --- perl scripts used in this makefile
       
     4 
       
     5 GENPAGE   = bin/genpage
       
     6 MKCONTENT = bin/mkcontents
       
     7 
       
     8 # ---
       
     9 # --- genpage stuff 
       
    10 
       
    11 # --- directories for main isabelle pages
       
    12 
       
    13 MAIN_CONTENT = main-content
       
    14 MAIN_LAYOUT  = main-layout
       
    15 MAIN_TARGET  = main
       
    16 
       
    17 # --- directories for isabelle distribution pages
       
    18 
       
    19 DIST_CONTENT = dist-content
       
    20 DIST_LAYOUT  = dist-layout
       
    21 DIST_TARGET  = dist
       
    22 
       
    23 # --- name of genpage template file
       
    24 TEMPLATE_NAME = template.html
       
    25 
       
    26 # ---
       
    27 # --- doc content generation
       
    28 
       
    29 # --- location of the Contents file of the Isabelle documentation
       
    30 DOC_CONTENT_FILE = ../../Distribution/doc/Contents
       
    31 
       
    32 # --- url prefixes for documentation links in main and dist dirs
       
    33 DIST_DOCU_PREFIX = $(DISTNAME)/doc/
       
    34 MAIN_DOCU_PREFIX = dist/$(DISTNAME)/doc/
       
    35 
       
    36 # --- target include files with documentation links
       
    37 DOC_CONTENTS_MAIN = docu-contents.main
       
    38 DOC_CONTENTS_DIST = docu-contents.dist
       
    39 
       
    40 # ---
       
    41 # --- begin rules
       
    42 
       
    43 all: clean gen
       
    44 
       
    45 gen: main dist
       
    46 
       
    47 main: check
       
    48 	$(MKCONTENT) -p $(MAIN_DOCU_PREFIX) $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN)
       
    49 	$(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET)
       
    50 
       
    51 	cd $(MAIN_TARGET); perl -pi -e "s/{ISABELLE}/$(DISTNAME)/g;" *.html
       
    52 
       
    53 dist: check
       
    54 	$(MKCONTENT) -p $(DIST_DOCU_PREFIX) $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST)
       
    55 	$(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET)
       
    56 
       
    57 	cd $(DIST_TARGET); perl -pi -e "s/{ISABELLE}/$(DISTNAME)/g;" *.html
       
    58 
       
    59 clean: 
       
    60 	rm -rf $(MAIN_TARGET)
       
    61 	rm -rf $(DIST_TARGET)
       
    62 	rm -rf $(DOC_CONTENTS_MAIN)
       
    63 	rm -rf $(DOC_CONTENTS_DIST)
       
    64 	rm -f `find . -name "*~" -type f`
       
    65 
       
    66 check:
       
    67 	@if [ "$(DISTNAME)" = "" ]; then echo "Error: \$$DISTNAME not set."; exit 1; fi