8056
|
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
|
8132
|
48 |
$(MKCONTENT) -p $(MAIN_DOCU_PREFIX) Contents $(DOC_CONTENTS_MAIN)
|
8056
|
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
|