| author | paulson | 
| Fri, 19 Mar 2004 10:48:22 +0100 | |
| changeset 14475 | aa973ba84f69 | 
| parent 11239 | be12c6f1ea75 | 
| child 14582 | f0779f6fa7e8 | 
| 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  | 
| 8056 | 41  | 
|
| 
9920
 
9734f2717203
improved WWW page generation (still somewhat experimental);
 
wenzelm 
parents: 
8133 
diff
changeset
 | 
42  | 
main:  | 
| 
 
9734f2717203
improved WWW page generation (still somewhat experimental);
 
wenzelm 
parents: 
8133 
diff
changeset
 | 
43  | 
@$(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
 | 
44  | 
@env DISTNAME=`cat DISTNAME` \  | 
| 
 
9734f2717203
improved WWW page generation (still somewhat experimental);
 
wenzelm 
parents: 
8133 
diff
changeset
 | 
45  | 
$(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET)  | 
| 8056 | 46  | 
|
| 
9920
 
9734f2717203
improved WWW page generation (still somewhat experimental);
 
wenzelm 
parents: 
8133 
diff
changeset
 | 
47  | 
dist:  | 
| 
 
9734f2717203
improved WWW page generation (still somewhat experimental);
 
wenzelm 
parents: 
8133 
diff
changeset
 | 
48  | 
@$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST)  | 
| 
 
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 $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET)  | 
| 8056 | 51  | 
|
| 11239 | 52  | 
install: main dist  | 
| 10040 | 53  | 
@cp -R dist/. ..  | 
| 11239 | 54  | 
@mkdir -p ../../main-`cat DISTNAME`/.  | 
55  | 
@cp -R main/. ../../main-`cat DISTNAME`/.  | 
|
| 10040 | 56  | 
|
| 10084 | 57  | 
weblint:  | 
| 10091 | 58  | 
-weblint -x netscape $(MAIN_TARGET)  | 
59  | 
-weblint -x netscape $(DIST_TARGET)  | 
|
| 10084 | 60  | 
|
| 8056 | 61  | 
clean:  | 
| 
9920
 
9734f2717203
improved WWW page generation (still somewhat experimental);
 
wenzelm 
parents: 
8133 
diff
changeset
 | 
62  | 
@rm -rf $(MAIN_TARGET)  | 
| 
 
9734f2717203
improved WWW page generation (still somewhat experimental);
 
wenzelm 
parents: 
8133 
diff
changeset
 | 
63  | 
@rm -rf $(DIST_TARGET)  | 
| 
 
9734f2717203
improved WWW page generation (still somewhat experimental);
 
wenzelm 
parents: 
8133 
diff
changeset
 | 
64  | 
@rm -rf $(DOC_CONTENTS_MAIN)  | 
| 
 
9734f2717203
improved WWW page generation (still somewhat experimental);
 
wenzelm 
parents: 
8133 
diff
changeset
 | 
65  | 
@rm -rf $(DOC_CONTENTS_DIST)  | 
| 
 
9734f2717203
improved WWW page generation (still somewhat experimental);
 
wenzelm 
parents: 
8133 
diff
changeset
 | 
66  | 
@find . -name "*~" -type f -print | xargs rm -f  |