# HG changeset patch # User haftmann # Date 1118060067 -7200 # Node ID 322e2a3335d4c43e2e0f44d2892ab8bbbde6b15f # Parent f9f2e16435936157b39f7d87652d349991d8520b (cvs removed) diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/Contents --- a/Admin/page/Contents Mon Jun 06 14:12:07 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -Learning Isabelle - tutorial Tutorial on Isabelle/HOL - isar-overview Tutorial on Isar - locales Tutorial on Locales - -Reference Manuals - isar-ref The Isabelle/Isar Reference Manual - ref The Isabelle Reference Manual - system The Isabelle System Manual - -Logics - logics Isabelle's Logics: overview and misc logics - logics-HOL Isabelle's Logics: HOL - logics-ZF Isabelle's Logics: FOL and ZF - -Specific Topics - axclass Tutorial on Axiomatic Type Classes - ind-defs (Co)Inductive Definitions in ZF diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/DISTNAME --- a/Admin/page/DISTNAME Mon Jun 06 14:12:07 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -Isabelle2004 diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/HOWTO --- a/Admin/page/HOWTO Mon Jun 06 14:12:07 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,63 +0,0 @@ -This file describes how to change and regenerate the Isabelle web pages. -See the bottom of the file for a short overview of the setup. - -== Changes to main == - -To make changes to the content of the main pages: - - * Edit or add the appropriate Admin/page/main-content/*.content files - * Run "make clean main" in Admin/page/ - * Check generated html in Admin/page/main/ - * Check changes in main-content into cvs - * Run "make pub-main" to publish to the Munich web site - * Run "mirror-main" in Cambridge to synchronize - - -== Changes to dist == - -These should be rare and are a bit more involved at the moment. The -principle is the same as for the main pages, but the script needs -access to the distribution files to calculate sizes etc: - - * Edit or add the appropriate Admin/page/dist-content/*.content files - * Make sure the Isabelle package files are available in directory Admin/page. - On sunbroy2, the following does the trick (in directory Admin/page): - - ln -s /home/html/isabelle/html-data/dist/contrib - for f in /home/html/isabelle/html-data/dist/*.tar.gz; do ln -s $f; done - - * Run "make clean dist" in Admin/page/ - * Check generated html in Admin/page/dist/ - * Check changes in dist-content into cvs - * Run "make pub-dist" to publish to the Munich web site - (will only copy *.html files, will not update other distribution files) - * Run "mirror-dist" in Cambridge and notify other mirrors to synchronize - - -== Overview == - -The pages are separated into two sets: - * main, for the main home page in Munich and Cambridge, and - * dist, for the current Isabelle distribution more widely mirrored. - -Both are generated by a script (genpage) that takes *.content files and -puts them into a common template. - -This is supposed to achieve the following: - * separation of layout and content - * automatic consistency between contents of distribution and web - page, including name of the distribution, file sizes of download - packages, and documentation generated from isabelle/Doc - -For this the web page generation script needs access to the following -support files: - -Admin/page/DISTNAME (name of the distribution, e.g. Isabelle2004) -Admin/page/Contents (same as Distribution/doc/Contents at the time - of the Isabelle release) - -Both files are set to the right values automatically by makedist when -the Isabelle distribution is generated and maintained manually in -between releases by the release manager in Admin/page in CVS. (In -between releases Admin/page/Contents can be different from -Distribution/doc/Contents) diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/Makefile --- a/Admin/page/Makefile Mon Jun 06 14:12:07 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,99 +0,0 @@ -# -- makefile for Isabelle web pages (dist and main) -# -- $Id$ - -# --- force shell -SHELL=bash - -# --- check parameters -ifeq ($(tidy),) - TIDYCMD=: -else - TIDYCMD=tidy -q -i -asxhtml --doctype auto --indent-spaces 2 --wrap 80 \ - --logical-emphasis yes --gnu-emacs yes --write-back yes -endif - -# --- external tools - -GENPAGE = ./bin/genpage -MKCONTENT = ./bin/mkcontents - -# --- -# --- genpage stuff - -# --- directories for main isabelle pages - -MAIN_CONTENT = main-content -MAIN_LAYOUT = main-layout -MAIN_TARGET = main - -# --- directories for isabelle distribution pages - -DIST_CONTENT = dist-content -DIST_LAYOUT = dist-layout -DIST_TARGET = dist - -# --- name of genpage template file -TEMPLATE_NAME = template.html - -# --- -# --- doc content generation - -# --- location of the Contents file of the Isabelle documentation -DOC_CONTENT_FILE = Contents - -# --- target include files with documentation links -DOC_CONTENTS_MAIN = docu-contents.main -DOC_CONTENTS_DIST = docu-contents.dist - -# --- target directories for publishing to web site -MAIN_PUB_MIRROR_SRC=sunbroy2.informatik.tu-muenchen.de:/home/proj/isabelle-repository/www/ -MAIN_PUB_DEST=sunbroy2.informatik.tu-muenchen.de:/home/html/isabelle/html-data/ -DIST_PUB_DEST=sunbroy2.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/ - -# --- -# --- begin rules - -all: clean main dist install weblint - -main: - @$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN) - @env DISTNAME=`cat DISTNAME` \ - $(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET) - -@cd $(MAIN_TARGET); \ - for html in *.html; \ - do $(TIDYCMD) $$html; \ - done - -pub-main: main - @echo "Publishing main pages (*.html only)." - scp main/*.html $(MAIN_PUB_MIRROR_SRC) - scp main/*.html $(MAIN_PUB_DEST) - -dist: - @$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST) - @env DISTNAME=`cat DISTNAME` \ - $(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET) - -@cd $(MAIN_TARGET); \ - for html in *.html; \ - do $(TIDYCMD) $$html; \ - done - -pub-dist: dist - @echo "Publishing dist pages (*.html only)." - scp dist/*.html $(DIST_PUB_DEST) - -install: main dist - @cp -R dist/. .. - @mkdir -p ../../main-`cat DISTNAME`/. - @cp -R main/. ../../main-`cat DISTNAME`/. - -weblint: - -weblint -x netscape -d extension-attribute -e img-size $(MAIN_TARGET) - -weblint -x netscape -d extension-attribute -e img-size $(DIST_TARGET) - -clean: - @rm -rf $(MAIN_TARGET) - @rm -rf $(DIST_TARGET) - @rm -rf $(DOC_CONTENTS_MAIN) - @rm -rf $(DOC_CONTENTS_DIST) - @find . -name "*~" -type f -print | xargs rm -f diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/bin/genpage --- a/Admin/page/bin/genpage Mon Jun 06 14:12:07 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,420 +0,0 @@ -#!/usr/bin/perl -w - -# Genpage - Webpage Generator. -# -# Copyright (C) Joe Vaughan 1998-1999 -# Some portions Copyright (C) Ronan Waide 1999 -# Some portions Copyright (C) Rocco Caputo 1999 -# -# This program is free software; you can redistribute it and/or modify -# it under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 2 of the License, or -# (at your option) any later version. -# -# This program is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY; without even the implied warranty of -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -# GNU General Public License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program; if not, write to the Free Software -# Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. - -$|=1; - -$version = "1.0b3"; - -# following fix for Mac Perl submitted by Dair Grant -# I shoulda thought of this, but I don't have a mac :) Thanks Dair. -# -# dair, construct a path procedurally -sub build_path -{ - - # Retrieve our parameters - # - my $thePath = $_[0]; - my $theItem = $_[1]; - - - - # If we're running on a Mac, munge the path/item/separator - # - if ($^O eq "MacOS") - { - $thePath =~ s/:$//; # Strip off trailing ':' - $theItem =~ s/^:$//; # Drop theItem == ':' - $pathDiv = ":"; # Use Mac separator - } - else - { - $pathDiv = "/"; # Use Unix separator - } - - - - # Return the path to the item - # - return($thePath . $pathDiv . $theItem); -} - - - -# Some handy variables. -$numfiles = 0; -$numcontentfiles = 0; -$numignoredfiles = 0; -$numskippedfiles = 0; -$numcpfiles = 0; -$numdirfiles =0; - -use Getopt::Std; -use File::Find; -use File::Copy 'cp'; - -# Current Working Dir. -$pwd = `pwd`; -chomp ($pwd); - -getopts('dt:c:o:fqhi:') || die "Invalid args, use $0 -h for help\n"; - -# $opt_d is debug flag -# $opt_t is template file. If not set, use standard template. -# $opt_c is content directory. If not set, use standard content dir. -# $opt_o is output dir, if not set, use standard output dir. -# $opt_q sets quiet mode (no stdout output) -# $opt_f sets a force flag - force generation even if output file is present -# and newer. -# $opt_h runs usage and exits - -# dair, build paths procedurally -$opt_t ||= build_path("", "layout") . build_path("", "template.html"); -$opt_c ||= build_path("", "content"); -$opt_o ||= build_path("", "www"); -$opt_f ||= 0; -$opt_d ||= 0; -$opt_q ||= 0; -$opt_h ||= 0; -$opt_i ||= 'CVS|.*,v$'; - -# dair, build paths procedurally -$opt_t = build_path($pwd, $opt_t); -$opt_c = build_path($pwd, $opt_c); -$opt_o = build_path($pwd, $opt_o); - - -if ($opt_h) { &usage; } - -if (!$opt_q) { - print "Genpage, version $version starting run...\n"; -} - -if ($opt_d) { print "pwd = $pwd\n"; } - -#Swallow template file whole... -open( TEMPLATE, "<$opt_t" ) || die "Can\'t open template file $opt_t: $!\n"; -{ -local $/; -undef $/; -$template =