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