Admin/page/Makefile
author haftmann
Mon, 06 Jun 2005 14:12:07 +0200
changeset 16301 f9f2e1643593
parent 15933 7f3ccb84e60d
permissions -rw-r--r--
migrated scripts to new webiste
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8133
ba1498046ee6 Id line inserted
kleing
parents: 8132
diff changeset
     1
# -- makefile for Isabelle web pages (dist and main)
ba1498046ee6 Id line inserted
kleing
parents: 8132
diff changeset
     2
# -- $Id$
ba1498046ee6 Id line inserted
kleing
parents: 8132
diff changeset
     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
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    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
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    19
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    20
# ---
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    21
# --- genpage stuff 
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    22
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    23
# --- directories for main isabelle pages
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    24
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    25
MAIN_CONTENT = main-content
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    26
MAIN_LAYOUT  = main-layout
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    27
MAIN_TARGET  = main
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    28
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    29
# --- directories for isabelle distribution pages
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    30
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    31
DIST_CONTENT = dist-content
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    32
DIST_LAYOUT  = dist-layout
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    33
DIST_TARGET  = dist
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    34
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    35
# --- name of genpage template file
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    36
TEMPLATE_NAME = template.html
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    37
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    38
# ---
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    39
# --- doc content generation
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    40
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    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
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    43
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    44
# --- target include files with documentation links
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    45
DOC_CONTENTS_MAIN = docu-contents.main
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    46
DOC_CONTENTS_DIST = docu-contents.dist
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    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
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    53
# ---
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    54
# --- begin rules
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    55
10084
ede64d0782e5 weblint;
wenzelm
parents: 10040
diff changeset
    56
all: clean main dist install weblint
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    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
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    66
15810
2c119fed01f0 howto for changing web pages, simplified makefile access
kleing
parents: 14582
diff changeset
    67
pub-main: main
15886
c5d873a86e0f publish only *.html
kleing
parents: 15810
diff changeset
    68
	@echo "Publishing main pages (*.html only)."
c5d873a86e0f publish only *.html
kleing
parents: 15810
diff changeset
    69
	scp main/*.html $(MAIN_PUB_MIRROR_SRC)
c5d873a86e0f publish only *.html
kleing
parents: 15810
diff changeset
    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
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    80
15810
2c119fed01f0 howto for changing web pages, simplified makefile access
kleing
parents: 14582
diff changeset
    81
pub-dist: dist
15886
c5d873a86e0f publish only *.html
kleing
parents: 15810
diff changeset
    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
wenzelm
parents: 10096
diff changeset
    85
install: main dist
10040
4642c9d62aeb added "install" target;
wenzelm
parents: 9920
diff changeset
    86
	@cp -R dist/. ..
11239
wenzelm
parents: 10096
diff changeset
    87
	@mkdir -p ../../main-`cat DISTNAME`/.
wenzelm
parents: 10096
diff changeset
    88
	@cp -R main/. ../../main-`cat DISTNAME`/.
10040
4642c9d62aeb added "install" target;
wenzelm
parents: 9920
diff changeset
    89
10084
ede64d0782e5 weblint;
wenzelm
parents: 10040
diff changeset
    90
weblint:
14582
f0779f6fa7e8 make weblint happy
kleing
parents: 11239
diff changeset
    91
	-weblint -x netscape -d extension-attribute -e img-size $(MAIN_TARGET)
f0779f6fa7e8 make weblint happy
kleing
parents: 11239
diff changeset
    92
	-weblint -x netscape -d extension-attribute -e img-size $(DIST_TARGET)
10084
ede64d0782e5 weblint;
wenzelm
parents: 10040
diff changeset
    93
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    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