author | kleing |
Fri, 22 Apr 2005 02:03:52 +0200 | |
changeset 15810 | 2c119fed01f0 |
parent 14582 | f0779f6fa7e8 |
child 15886 | c5d873a86e0f |
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 |
||
15810
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
37 |
# --- target directories for publishing to web site |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
38 |
MAIN_PUB_MIRROR_SRC=sunbroy2.informatik.tu-muenchen.de:/home/proj/isabelle-repository/www/ |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
39 |
MAIN_PUB_DEST=sunbroy2.informatik.tu-muenchen.de:/home/html/isabelle/html-data/ |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
40 |
DIST_PUB_DEST=sunbroy2.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/ |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
41 |
|
8056 | 42 |
# --- |
43 |
# --- begin rules |
|
44 |
||
10084 | 45 |
all: clean main dist install weblint |
8056 | 46 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
47 |
main: |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
48 |
@$(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
|
49 |
@env DISTNAME=`cat DISTNAME` \ |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
50 |
$(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET) |
8056 | 51 |
|
15810
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
52 |
pub-main: main |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
53 |
@echo "Publishing main pages." |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
54 |
scp main/* $(MAIN_PUB_MIRROR_SRC) |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
55 |
scp main/* $(MAIN_PUB_DEST) |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
56 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
57 |
dist: |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
58 |
@$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
59 |
@env DISTNAME=`cat DISTNAME` \ |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
60 |
$(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET) |
8056 | 61 |
|
15810
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
62 |
pub-dist: dist |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
63 |
@echo "Publishing dist pages." |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
64 |
scp dist/*.html $(DIST_PUB_DEST) |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
65 |
|
11239 | 66 |
install: main dist |
10040 | 67 |
@cp -R dist/. .. |
11239 | 68 |
@mkdir -p ../../main-`cat DISTNAME`/. |
69 |
@cp -R main/. ../../main-`cat DISTNAME`/. |
|
10040 | 70 |
|
10084 | 71 |
weblint: |
14582 | 72 |
-weblint -x netscape -d extension-attribute -e img-size $(MAIN_TARGET) |
73 |
-weblint -x netscape -d extension-attribute -e img-size $(DIST_TARGET) |
|
10084 | 74 |
|
8056 | 75 |
clean: |
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
76 |
@rm -rf $(MAIN_TARGET) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
77 |
@rm -rf $(DIST_TARGET) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
78 |
@rm -rf $(DOC_CONTENTS_MAIN) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
79 |
@rm -rf $(DOC_CONTENTS_DIST) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
80 |
@find . -name "*~" -type f -print | xargs rm -f |