author | wenzelm |
Tue, 26 Sep 2000 18:27:50 +0200 | |
changeset 10091 | 43c1951a369c |
parent 10084 | ede64d0782e5 |
child 10096 | 6cbe69107c18 |
permissions | -rw-r--r-- |
8133 | 1 |
# -- makefile for Isabelle web pages (dist and main) |
2 |
# -- $Id$ |
|
3 |
||
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
4 |
# --- external tools |
8056 | 5 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
6 |
GENPAGE = ./bin/genpage |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
7 |
MKCONTENT = ./bin/mkcontents |
8056 | 8 |
|
9 |
# --- |
|
10 |
# --- genpage stuff |
|
11 |
||
12 |
# --- directories for main isabelle pages |
|
13 |
||
14 |
MAIN_CONTENT = main-content |
|
15 |
MAIN_LAYOUT = main-layout |
|
16 |
MAIN_TARGET = main |
|
17 |
||
18 |
# --- directories for isabelle distribution pages |
|
19 |
||
20 |
DIST_CONTENT = dist-content |
|
21 |
DIST_LAYOUT = dist-layout |
|
22 |
DIST_TARGET = dist |
|
23 |
||
24 |
# --- name of genpage template file |
|
25 |
TEMPLATE_NAME = template.html |
|
26 |
||
27 |
# --- |
|
28 |
# --- doc content generation |
|
29 |
||
30 |
# --- location of the Contents file of the Isabelle documentation |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
31 |
DOC_CONTENT_FILE = Contents |
8056 | 32 |
|
33 |
# --- target include files with documentation links |
|
34 |
DOC_CONTENTS_MAIN = docu-contents.main |
|
35 |
DOC_CONTENTS_DIST = docu-contents.dist |
|
36 |
||
37 |
# --- |
|
38 |
# --- begin rules |
|
39 |
||
10084 | 40 |
all: clean main dist install weblint |
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
41 |
@echo "###" |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
42 |
@echo "### Finished. See main/ and dist/ for the resulting pages." |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
43 |
@echo "###" |
8056 | 44 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
45 |
main: |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
46 |
@$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
47 |
@env DISTNAME=`cat DISTNAME` \ |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
48 |
$(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET) |
8056 | 49 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
50 |
dist: |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
51 |
@$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
52 |
@env DISTNAME=`cat DISTNAME` \ |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
53 |
$(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET) |
8056 | 54 |
|
10040 | 55 |
install: dist |
56 |
@cp -R dist/. .. |
|
57 |
||
10084 | 58 |
weblint: |
10091 | 59 |
-weblint -x netscape $(MAIN_TARGET) |
60 |
-weblint -x netscape $(DIST_TARGET) |
|
10084 | 61 |
|
8056 | 62 |
clean: |
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
63 |
@rm -rf $(MAIN_TARGET) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
64 |
@rm -rf $(DIST_TARGET) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
65 |
@rm -rf $(DOC_CONTENTS_MAIN) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
66 |
@rm -rf $(DOC_CONTENTS_DIST) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
67 |
@find . -name "*~" -type f -print | xargs rm -f |