author | kleing |
Fri, 27 May 2005 01:09:44 +0200 | |
changeset 16095 | f6af6b265d20 |
parent 15933 | 7f3ccb84e60d |
permissions | -rw-r--r-- |
8133 | 1 |
# -- makefile for Isabelle web pages (dist and main) |
2 |
# -- $Id$ |
|
3 |
||
15933
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
4 |
# --- force shell |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
5 |
SHELL=bash |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
6 |
|
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
7 |
# --- check parameters |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
8 |
ifeq ($(tidy),) |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
9 |
TIDYCMD=: |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
10 |
else |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
11 |
TIDYCMD=tidy -q -i -asxhtml --doctype auto --indent-spaces 2 --wrap 80 \ |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
12 |
--logical-emphasis yes --gnu-emacs yes --write-back yes |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
13 |
endif |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
14 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
15 |
# --- external tools |
8056 | 16 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
17 |
GENPAGE = ./bin/genpage |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
18 |
MKCONTENT = ./bin/mkcontents |
8056 | 19 |
|
20 |
# --- |
|
21 |
# --- genpage stuff |
|
22 |
||
23 |
# --- directories for main isabelle pages |
|
24 |
||
25 |
MAIN_CONTENT = main-content |
|
26 |
MAIN_LAYOUT = main-layout |
|
27 |
MAIN_TARGET = main |
|
28 |
||
29 |
# --- directories for isabelle distribution pages |
|
30 |
||
31 |
DIST_CONTENT = dist-content |
|
32 |
DIST_LAYOUT = dist-layout |
|
33 |
DIST_TARGET = dist |
|
34 |
||
35 |
# --- name of genpage template file |
|
36 |
TEMPLATE_NAME = template.html |
|
37 |
||
38 |
# --- |
|
39 |
# --- doc content generation |
|
40 |
||
41 |
# --- location of the Contents file of the Isabelle documentation |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
42 |
DOC_CONTENT_FILE = Contents |
8056 | 43 |
|
44 |
# --- target include files with documentation links |
|
45 |
DOC_CONTENTS_MAIN = docu-contents.main |
|
46 |
DOC_CONTENTS_DIST = docu-contents.dist |
|
47 |
||
15810
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
48 |
# --- target directories for publishing to web site |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
49 |
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
|
50 |
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
|
51 |
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
|
52 |
|
8056 | 53 |
# --- |
54 |
# --- begin rules |
|
55 |
||
10084 | 56 |
all: clean main dist install weblint |
8056 | 57 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
58 |
main: |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
59 |
@$(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
|
60 |
@env DISTNAME=`cat DISTNAME` \ |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
61 |
$(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET) |
15933
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
62 |
-@cd $(MAIN_TARGET); \ |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
63 |
for html in *.html; \ |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
64 |
do $(TIDYCMD) $$html; \ |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
65 |
done |
8056 | 66 |
|
15810
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
67 |
pub-main: main |
15886 | 68 |
@echo "Publishing main pages (*.html only)." |
69 |
scp main/*.html $(MAIN_PUB_MIRROR_SRC) |
|
70 |
scp main/*.html $(MAIN_PUB_DEST) |
|
15810
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
71 |
|
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
72 |
dist: |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
73 |
@$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
74 |
@env DISTNAME=`cat DISTNAME` \ |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
75 |
$(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET) |
15933
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
76 |
-@cd $(MAIN_TARGET); \ |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
77 |
for html in *.html; \ |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
78 |
do $(TIDYCMD) $$html; \ |
7f3ccb84e60d
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
haftmann
parents:
15886
diff
changeset
|
79 |
done |
8056 | 80 |
|
15810
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
81 |
pub-dist: dist |
15886 | 82 |
@echo "Publishing dist pages (*.html only)." |
15810
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
83 |
scp dist/*.html $(DIST_PUB_DEST) |
2c119fed01f0
howto for changing web pages, simplified makefile access
kleing
parents:
14582
diff
changeset
|
84 |
|
11239 | 85 |
install: main dist |
10040 | 86 |
@cp -R dist/. .. |
11239 | 87 |
@mkdir -p ../../main-`cat DISTNAME`/. |
88 |
@cp -R main/. ../../main-`cat DISTNAME`/. |
|
10040 | 89 |
|
10084 | 90 |
weblint: |
14582 | 91 |
-weblint -x netscape -d extension-attribute -e img-size $(MAIN_TARGET) |
92 |
-weblint -x netscape -d extension-attribute -e img-size $(DIST_TARGET) |
|
10084 | 93 |
|
8056 | 94 |
clean: |
9920
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
95 |
@rm -rf $(MAIN_TARGET) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
96 |
@rm -rf $(DIST_TARGET) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
97 |
@rm -rf $(DOC_CONTENTS_MAIN) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
98 |
@rm -rf $(DOC_CONTENTS_DIST) |
9734f2717203
improved WWW page generation (still somewhat experimental);
wenzelm
parents:
8133
diff
changeset
|
99 |
@find . -name "*~" -type f -print | xargs rm -f |