improved WWW page generation (still somewhat experimental);
authorwenzelm
Mon, 11 Sep 2000 17:41:34 +0200
changeset 99209734f2717203
parent 9919 3cf12ab0b8ac
child 9921 7acefd99e748
improved WWW page generation (still somewhat experimental);
Admin/filesizes
Admin/makedist
Admin/page/Makefile
Admin/page/bin/genpage
Admin/page/common/functions.pl
Admin/page/dist-content/binary.content
Admin/page/dist-content/docs.content
Admin/page/dist-content/index.content
Admin/page/dist-content/past.content
Admin/page/dist-content/source.content
Admin/page/dist-layout/navigation.html
Admin/page/main-content/docs.content
Admin/page/main-content/index.content
Admin/page/main-layout/navigation.html
     1.1 --- a/Admin/filesizes	Mon Sep 11 17:40:41 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,94 +0,0 @@
     1.4 -#!/bin/bash
     1.5 -#
     1.6 -# $Id$
     1.7 -#
     1.8 -# filesizes -- calculate and substitute file sizes in isabelle web pages
     1.9 -#
    1.10 -# needs:
    1.11 -# working directory in dist, rpms + webpages generated and copied to dist
    1.12 -# $DISTNAME
    1.13 -# 
    1.14 -# substitutes:
    1.15 -# -norpm:
    1.16 -# {PACKED_SIZE} {PACKED_SIZE_PDF} {UNPACKED_SIZE}
    1.17 -# -rpm:
    1.18 -# {RPM_SML_SIZE} {RPM_BASE_SIZE} {RPM_HOL_SIZE} {RPM_REAL_SIZE}
    1.19 -# {RPM_ZF_SIZE} {RPM_DOCS_SIZE}
    1.20 -
    1.21 -
    1.22 -PRG=$(basename $0)
    1.23 -
    1.24 -function usage()
    1.25 -{
    1.26 -  echo
    1.27 -  echo "Usage: $PRG [-rpm|-norpm]"
    1.28 -  echo
    1.29 -  echo "fill in file sizes and distname in isabelle dist web pages"
    1.30 -  echo
    1.31 -  echo "  Options are:"
    1.32 -  echo "    -rpm     only fill in rpm sizes"
    1.33 -  echo "    -norpm   only fille in other sizes"
    1.34 -  echo "  (do both by default)" 
    1.35 -  echo 
    1.36 -  echo "needs \$DISTNAME environment variable"
    1.37 -  echo "expects to be startet in isabelle dist dir"
    1.38 -  echo
    1.39 -  exit 1
    1.40 -}
    1.41 -
    1.42 -function fail()
    1.43 -{
    1.44 -  echo "$1" >&2
    1.45 -  exit 2
    1.46 -}
    1.47 -
    1.48 -# check options
    1.49 -
    1.50 -if [ $# -ge 2 ]; then
    1.51 -  usage
    1.52 -fi
    1.53 -
    1.54 -if [ $# -eq 1 -a "$1" != "-rpm" -a "$1" != "-norpm" ]; then
    1.55 -  usage
    1.56 -fi
    1.57 -
    1.58 -
    1.59 -# begin work
    1.60 -
    1.61 -if [ $# -eq 0 -o "$1" = "-norpm" ]; then
    1.62 -
    1.63 -  # check for $DISTNAME
    1.64 -  if [ "$DISTNAME" = "" ]; then    
    1.65 -    echo "Error: \$DISTNAME not set"
    1.66 -    usage
    1.67 -  fi
    1.68 -
    1.69 -  PACKED_SIZE=$[ $(wc -c < $DISTNAME.tar.gz) / 1024 ]
    1.70 -  PACKED_SIZE_PDF=$[ $(wc -c < ${DISTNAME}_pdf.tar.gz) / 1024 ]
    1.71 -
    1.72 -  UNPACKED_SIZE=$[ $(cat $DISTNAME.tar.gz ${DISTNAME}_pdf.tar.gz | gunzip | wc -c) / 1024 ]
    1.73 -
    1.74 -  perl -pi -e \
    1.75 -   "s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \ 
    1.76 -    s/{PACKED_SIZE}/$PACKED_SIZE/g; \
    1.77 -    s/{PACKED_SIZE_PDF}/$PACKED_SIZE_PDF/g;" \
    1.78 -      *.html
    1.79 -fi
    1.80 -
    1.81 -if [ $# -eq 0 -o "$1" = "-rpm" ]; then
    1.82 -  RPM_SML_SIZE=$[ $(wc -c < rpm/polyml-3X-1.i386.rpm) / 1024 ]
    1.83 -  RPM_BASE_SIZE=$[ $(wc -c < rpm/isabelle.rpm) / 1024 ]
    1.84 -  RPM_HOL_SIZE=$[ $(wc -c < rpm/isabelle-HOL.i386.rpm) / 1024 ]
    1.85 -  RPM_REAL_SIZE=$[ $(wc -c < rpm/isabelle-HOL-Real.i386.rpm) / 1024 ]
    1.86 -  RPM_ZF_SIZE=$[ $(wc -c < rpm/isabelle-ZF.i386.rpm) / 1024 ]
    1.87 -  RPM_DOCS_SIZE=$[ $(wc -c < rpm/isabelle-pdfdocs.rpm) / 1024 ]
    1.88 -
    1.89 -  perl -pi -e \
    1.90 -   "s/{RPM_SML_SIZE}/$RPM_SML_SIZE/g; \
    1.91 -    s/{RPM_BASE_SIZE}/$RPM_BASE_SIZE/g; \
    1.92 -    s/{RPM_HOL_SIZE}/$RPM_HOL_SIZE/g; \
    1.93 -    s/{RPM_REAL_SIZE}/$RPM_REAL_SIZE/g; \
    1.94 -    s/{RPM_ZF_SIZE}/$RPM_ZF_SIZE/g; \
    1.95 -    s/{RPM_DOCS_SIZE}/$RPM_DOCS_SIZE/g;" \
    1.96 -      *.html
    1.97 -fi
     2.1 --- a/Admin/makedist	Mon Sep 11 17:40:41 2000 +0200
     2.2 +++ b/Admin/makedist	Mon Sep 11 17:41:34 2000 +0200
     2.3 @@ -14,6 +14,12 @@
     2.4  
     2.5  umask 022
     2.6  
     2.7 +TAR=tar
     2.8 +type -path gtar >/dev/null && TAR=gtar
     2.9 +
    2.10 +FIND=find
    2.11 +type -path gfind >/dev/null && FIND=gfind
    2.12 +
    2.13  
    2.14  ## diagnostics
    2.15  
    2.16 @@ -110,10 +116,10 @@
    2.17  cd "$DISTBASE"
    2.18  
    2.19  $EXPORT
    2.20 -find . -name CVS -print | xargs rm -rf
    2.21 -find . "(" -type d -a -empty ")" -print | xargs rm -f
    2.22 -find . "(" -type d -a -empty ")" -print | xargs rm -f
    2.23 -find . "(" -type d -a -empty ")" -print | xargs rm -f
    2.24 +$FIND . -name CVS -print | xargs rm -rf
    2.25 +$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
    2.26 +$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
    2.27 +$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
    2.28  
    2.29  
    2.30  # build docs
    2.31 @@ -128,24 +134,27 @@
    2.32  for DOC in $(cat Contents)
    2.33  do
    2.34    cd "$DOC"
    2.35 -  make dvi
    2.36 -  [ -n "$PDFLATEX" ] && make clean pdf
    2.37 +  #FIXME make dvi
    2.38 +  #FIXME [ -n "$PDFLATEX" ] && make clean pdf
    2.39    cd ..
    2.40  done
    2.41  
    2.42  
    2.43 -# make WWW pages
    2.44 +# prepare dist dir for release
    2.45  
    2.46 -#FIXME
    2.47 -#export DISTNAME
    2.48 -#( cd "$DISTBASE/$DISTNAME/Admin/page"; make clean; make dist; cd dist; cp * "$DISTBASE"; )
    2.49 -
    2.50 -
    2.51 -# prepare dist dir for release
    2.52 +echo "###"
    2.53 +echo "### Preparing distribution ..."
    2.54 +echo "###"
    2.55  
    2.56  cd "$DISTBASE/$DISTNAME"
    2.57  
    2.58 -MOVE=$(find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
    2.59 +cp -R Admin/page ../page
    2.60 +cp Distribution/Doc/Contents ../page/Contents
    2.61 +cp Distribution/lib/logo/isabelle.gif ../page/main-content
    2.62 +cp Distribution/lib/logo/isabelle.gif ../page/dist-content
    2.63 +echo "$DISTNAME" > ../page/DISTNAME
    2.64 +
    2.65 +MOVE=$($FIND Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
    2.66  mv -f $MOVE Distribution/doc
    2.67  rm Distribution/doc/Isa-logics.eps
    2.68  rm -rf Doc Tools
    2.69 @@ -194,9 +203,6 @@
    2.70  chmod -R u+w "$DISTNAME"
    2.71  chmod -R g=o "$DISTNAME"
    2.72  
    2.73 -TAR=tar
    2.74 -type -path gtar >/dev/null && TAR=gtar
    2.75 -
    2.76  mkdir -p "pdf/$DISTNAME/doc"
    2.77  mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
    2.78  
    2.79 @@ -215,7 +221,6 @@
    2.80  mv "$DISTNAME" "${DISTNAME}-old"
    2.81  mkdir "$DISTNAME"
    2.82  
    2.83 -mv "${DISTNAME}-old/lib/logo/isabelle.gif" .
    2.84  mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "$DISTNAME"
    2.85  mkdir "$DISTNAME/doc"
    2.86  mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
    2.87 @@ -225,14 +230,8 @@
    2.88  rm -rf "${DISTNAME}-old"
    2.89  
    2.90  
    2.91 -# prepare web pages
    2.92 -
    2.93 -#FIXME
    2.94 -#$THIS/filesizes -norpm
    2.95 -
    2.96 -
    2.97  # final note
    2.98  
    2.99  echo "###"
   2.100 -echo "### Finished. You will find the distribution in $DISTBASE."
   2.101 +echo "### Finished."
   2.102  echo "###"
     3.1 --- a/Admin/page/Makefile	Mon Sep 11 17:40:41 2000 +0200
     3.2 +++ b/Admin/page/Makefile	Mon Sep 11 17:41:34 2000 +0200
     3.3 @@ -1,12 +1,10 @@
     3.4 -# --- uses $DISTNAME environment variable 
     3.5 -
     3.6  # -- makefile for Isabelle web pages (dist and main)
     3.7  # -- $Id$
     3.8  
     3.9 -# --- perl scripts used in this makefile
    3.10 +# --- external tools
    3.11  
    3.12 -GENPAGE   = bin/genpage
    3.13 -MKCONTENT = bin/mkcontents
    3.14 +GENPAGE   = ./bin/genpage
    3.15 +MKCONTENT = ./bin/mkcontents
    3.16  
    3.17  # ---
    3.18  # --- genpage stuff 
    3.19 @@ -30,11 +28,7 @@
    3.20  # --- doc content generation
    3.21  
    3.22  # --- location of the Contents file of the Isabelle documentation
    3.23 -DOC_CONTENT_FILE = ../../Distribution/doc/Contents
    3.24 -
    3.25 -# --- url prefixes for documentation links in main and dist dirs
    3.26 -DIST_DOCU_PREFIX = $(DISTNAME)/doc/
    3.27 -MAIN_DOCU_PREFIX = dist/$(DISTNAME)/doc/
    3.28 +DOC_CONTENT_FILE = Contents
    3.29  
    3.30  # --- target include files with documentation links
    3.31  DOC_CONTENTS_MAIN = docu-contents.main
    3.32 @@ -43,28 +37,24 @@
    3.33  # ---
    3.34  # --- begin rules
    3.35  
    3.36 -all: clean gen
    3.37 +all: clean main dist
    3.38 +	@echo "###"
    3.39 +	@echo "### Finished.  See main/ and dist/ for the resulting pages."
    3.40 +	@echo "###"
    3.41  
    3.42 -gen: main dist
    3.43 +main:
    3.44 +	@$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN)
    3.45 +	@env DISTNAME=`cat DISTNAME` \
    3.46 +	  $(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET)
    3.47  
    3.48 -main: check
    3.49 -	$(MKCONTENT) -p $(MAIN_DOCU_PREFIX) Contents $(DOC_CONTENTS_MAIN)
    3.50 -	$(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET)
    3.51 -
    3.52 -	cd $(MAIN_TARGET); perl -pi -e "s/{ISABELLE}/$(DISTNAME)/g;" *.html
    3.53 -
    3.54 -dist: check
    3.55 -	$(MKCONTENT) -p $(DIST_DOCU_PREFIX) $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST)
    3.56 -	$(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET)
    3.57 -
    3.58 -	cd $(DIST_TARGET); perl -pi -e "s/{ISABELLE}/$(DISTNAME)/g;" *.html
    3.59 +dist:
    3.60 +	@$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST)
    3.61 +	@env DISTNAME=`cat DISTNAME` \
    3.62 +	  $(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET)
    3.63  
    3.64  clean: 
    3.65 -	rm -rf $(MAIN_TARGET)
    3.66 -	rm -rf $(DIST_TARGET)
    3.67 -	rm -rf $(DOC_CONTENTS_MAIN)
    3.68 -	rm -rf $(DOC_CONTENTS_DIST)
    3.69 -	rm -f `find . -name "*~" -type f`
    3.70 -
    3.71 -check:
    3.72 -	@if [ "$(DISTNAME)" = "" ]; then echo "Error: \$$DISTNAME not set."; exit 1; fi
    3.73 +	@rm -rf $(MAIN_TARGET)
    3.74 +	@rm -rf $(DIST_TARGET)
    3.75 +	@rm -rf $(DOC_CONTENTS_MAIN)
    3.76 +	@rm -rf $(DOC_CONTENTS_DIST)
    3.77 +	@find . -name "*~" -type f -print | xargs rm -f
     4.1 --- a/Admin/page/bin/genpage	Mon Sep 11 17:40:41 2000 +0200
     4.2 +++ b/Admin/page/bin/genpage	Mon Sep 11 17:41:34 2000 +0200
     4.3 @@ -1,7 +1,4 @@
     4.4 -#!/bin/sh
     4.5 -exec perl -x. $0 ${1+"$@"} 
     4.6 -#
     4.7 -#!perl -w
     4.8 +#!/usr/bin/perl -w
     4.9  
    4.10  # Genpage - Webpage Generator.
    4.11  #
     5.1 --- a/Admin/page/common/functions.pl	Mon Sep 11 17:40:41 2000 +0200
     5.2 +++ b/Admin/page/common/functions.pl	Mon Sep 11 17:41:34 2000 +0200
     5.3 @@ -1,9 +1,12 @@
     5.4  <!-- _GP_
     5.5  # undef all the functions we're defining. This stops lots of
     5.6 -# complaining about re-defining the sub for each content file thats
     5.7 +# complaining about re-defining the sub for each content file that's
     5.8  # processed.
     5.9  
    5.10         if (defined(&me)) { undef &me; }
    5.11 +       if (defined(&distname)) { undef &distname; }
    5.12 +       if (defined(&href)) { undef &href; }
    5.13 +       if (defined(&twodig)) { undef &twodig; }
    5.14         if (defined(&when)) { undef &when; }
    5.15         if (defined(&size)) { undef &size; }
    5.16         if (defined(&page)) { undef &page; }
    5.17 @@ -17,6 +20,14 @@
    5.18  
    5.19  <!--  _GP_ 
    5.20  
    5.21 +    sub distname {
    5.22 +      return $ENV{"DISTNAME"};
    5.23 +    }
    5.24 +
    5.25 +    sub href {
    5.26 +	return "<a href=\"" . $_[0] . "\">" . $_[1] . "</a>";
    5.27 +    }
    5.28 +
    5.29      sub twodig {
    5.30        if ($_[0] < 10) {
    5.31          return "0$_[0]";
    5.32 @@ -85,9 +96,9 @@
    5.33      sub size {
    5.34        my $filename = $_[0];
    5.35        my @s = stat $filename;
    5.36 -      my $size = $s[7]/1024;
    5.37 +      my $size = defined $s[7] ? $s[7]/1024 : 0;
    5.38  
    5.39 -      return sprintf("%.1f",$size);
    5.40 +      return sprintf("%.1f", $size);
    5.41      }
    5.42  
    5.43      sub setdowncolor {
    5.44 @@ -95,17 +106,15 @@
    5.45        return "";
    5.46      }
    5.47  
    5.48 -   # download(description, url, size)
    5.49 +   # download(description, url, prefix)
    5.50      sub download {
    5.51  
    5.52        my $descr = $_[0];
    5.53        my $url   = $_[1];
    5.54 -      my $size  = $_[2];
    5.55 +      my $prefix  = $_[2];
    5.56  
    5.57 -      if ($size eq "") {
    5.58 -	$size = size($url);
    5.59 -	$size = "$size K";
    5.60 -      }
    5.61 +      my $size = size("$prefix/$url");
    5.62 +      $size = "$size K";
    5.63  
    5.64        my $filename = $path;
    5.65  
     6.1 --- a/Admin/page/dist-content/binary.content	Mon Sep 11 17:40:41 2000 +0200
     6.2 +++ b/Admin/page/dist-content/binary.content	Mon Sep 11 17:41:34 2000 +0200
     6.3 @@ -2,36 +2,83 @@
     6.4  Isabelle Binary Distribution
     6.5  
     6.6  %body%
     6.7 -The binary distribution of {ISABELLE} for rpm-based Linux/x86 systems:
     6.8 +
     6.9 +<h2>(1) Linux/x86 systems with RPM</h2>
    6.10 +
    6.11 +This is the binary distribution of <!-- _GP_ distname --> for
    6.12 +Linux/x86 systems.  It requires RPM based package management (as used
    6.13 +by most Linux distributions), and <em>root</em> user access to
    6.14 +install.
    6.15  
    6.16  <p>
    6.17  
    6.18  <!-- _GP_ setdowncolor("#E0E0E0") -->
    6.19  <center>
    6.20  <table border="0" cellspacing="5" cellpadding="4" width="520">
    6.21 -
    6.22 -  <!-- _GP_ download("ML system", "rpm/smlnj-110.0-3.i386.rpm", "{RPM_SML_SIZE} K") -->
    6.23 -  <!-- _GP_ download("Isabelle system", "rpm/isabelle.rpm", "{RPM_BASE_SIZE} K") -->
    6.24 -  <!-- _GP_ download("Isabelle/HOL image", "rpm/isabelle-HOL.i386.rpm", "{RPM_HOL_SIZE} K") -->
    6.25 -  <!-- _GP_ download("Isabelle/HOL-Real image (optional)", "rpm/isabelle-HOL-Real.i386.rpm", "{RPM_REAL_SIZE} K") -->
    6.26 -  <!-- _GP_ download("Isabelle/ZF image (optional)", "rpm/isabelle-ZF.i386.rpm", "{RPM_ZF_SIZE} K") -->
    6.27 -  <!-- _GP_ download("Isabelle pdf documentation (optional)", "rpm/isabelle-pdfdocs.rpm", "{RPM_DOCS_SIZE} K") -->
    6.28 -
    6.29 +  <!-- _GP_ download("Poly/ML system", "contrib/polyml.i386.rpm", "../..") -->
    6.30 +  <!-- _GP_ download("Isabelle main system", "isabelle.rpm", "../..") -->
    6.31 +  <!-- _GP_ download("Isabelle/HOL image", "isabelle-HOL.i386.rpm", "../..") -->
    6.32 +  <!-- _GP_ download("Isabelle/HOL-Real image (optional)", "isabelle-HOL-Real.i386.rpm", "../..") -->
    6.33 +  <!-- _GP_ download("Isabelle/ZF image (optional)", "isabelle-ZF.i386.rpm", "../..") -->
    6.34 +  <!-- _GP_ download("Isabelle pdf documentation (optional)", "isabelle-pdfdocs.rpm", "../..") -->
    6.35 +  <!-- _GP_ download("Proof General system (recommended)", "contrib/proofgeneral.rpm", "../..") -->
    6.36 +  <!-- _GP_ download("X-Symbol package (recommended)", "contrib/xsymbol.rpm", "../..") -->
    6.37  </table>
    6.38 -
    6.39  </center>
    6.40  
    6.41  <p>
    6.42  
    6.43 -Example installation procedure:
    6.44 +Example installation in <tt>/usr/share</tt> (the default location).
    6.45  
    6.46  <pre>
    6.47 -rpm -i smlnj-110.0-3.i386.rpm 
    6.48 -rpm -i --prefix /usr/share isabelle.rpm             
    6.49 -rpm -i --prefix /usr/share isabelle-HOL.i386.rpm    
    6.50 +rpm -i --prefix /usr/share polyml.i386.rpm
    6.51 +rpm -i --prefix /usr/share isabelle.rpm
    6.52 +rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
    6.53 +rpm -i --prefix /usr/share proofgeneral.rpm               #requires XEmacs-21
    6.54 +rpm -i --prefix /usr/share xsymbol.rpm                    #requires XEmacs-21
    6.55  </pre>
    6.56  
    6.57  <p>
    6.58  
    6.59 -Use the mailing list <a href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
    6.60 -to discuss problems and results.  (Why not <A HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?)
    6.61 +
    6.62 +<h2>(2) Generic Linux/x86 or Solaris/Sparc systems</h2>
    6.63 +
    6.64 +The following distribution of <!-- _GP_ distname --> works for any
    6.65 +Linux/x86 or Solaris/Sparc system -- only Poly/ML is platform
    6.66 +dependent.  Installation does not rely on package management; it may
    6.67 +be performed by non-root users as well.
    6.68 +
    6.69 +<p>
    6.70 +
    6.71 +<!-- _GP_ setdowncolor("#E0E0E0") -->
    6.72 +<center>
    6.73 +<table border="0" cellspacing="5" cellpadding="4" width="520">
    6.74 +  <!-- _GP_ download("Poly/ML base system", "contrib/polyml.tar.gz", "../..") -->
    6.75 +  <!-- _GP_ download("Poly/ML module for Linux/x86", "contrib/polyml_x86-linux.tar.gz", "../..") -->
    6.76 +  <!-- _GP_ download("Poly/ML module for Solaris/Sparc", "contrib/polyml_sparc-solaris.tar.gz", "../..") -->
    6.77 +  <!-- _GP_ download("Isabelle main system", distname . ".tar.gz", "../..") -->
    6.78 +  <!-- _GP_ download("Isabelle pdf documentation (optional)", distname . "_pdf.tar.gz", "../..") -->  <!-- _GP_ download("Proof General system (recommended)", "contrib/proofgeneral.tar.gz", "../..") -->
    6.79 +  <!-- _GP_ download("X-Symbol package (recommended)", "contrib/xsymbol.tar.gz", "../..") -->
    6.80 +</table>
    6.81 +</center>
    6.82 +
    6.83 +<p>
    6.84 +
    6.85 +Example installation in <tt>/usr/share</tt> for Linux/x86.
    6.86 +
    6.87 +<pre>
    6.88 +tar -C /usr/share -x -z -f polyml.tar.gz
    6.89 +tar -C /usr/share -x -z -f polyml_x86-linux.tar.gz
    6.90 +tar -C /usr/share -x -z -f <!-- _GP_ distname . ".tar.gz"-->
    6.91 +tar -C /usr/share -x -z -f proofgeneral.tar.gz            #requires XEmacs-21
    6.92 +tar -C /usr/share -x -z -f xsymbol.tar.gz                 #requires XEmacs-21
    6.93 +
    6.94 +cd <!-- _GP_ "/usr/share/" . distname -->
    6.95 +./configure
    6.96 +./build
    6.97 +./bin/isatool install -p /usr/bin
    6.98 +</pre>
    6.99 +
   6.100 +<p>
   6.101 +
   6.102 +<p>
     7.1 --- a/Admin/page/dist-content/docs.content	Mon Sep 11 17:40:41 2000 +0200
     7.2 +++ b/Admin/page/dist-content/docs.content	Mon Sep 11 17:41:34 2000 +0200
     7.3 @@ -6,4 +6,5 @@
     7.4  
     7.5  <!-- _GP_ include("$pwd/docu-contents.dist") -->
     7.6  
     7.7 -All this documentation is also part of the Isabelle <a href="source.html">distribution</a>.
     7.8 +All this documentation is also part of the Isabelle <a
     7.9 +href="source.html">distribution</a> (both as dvi and pdf).
     8.1 --- a/Admin/page/dist-content/index.content	Mon Sep 11 17:40:41 2000 +0200
     8.2 +++ b/Admin/page/dist-content/index.content	Mon Sep 11 17:41:34 2000 +0200
     8.3 @@ -21,5 +21,3 @@
     8.4  <li> <a href="ftp://rodin.stanford.edu/pub/smlnj/isabelle/source.html">Stanford (USA)</a> <br>&nbsp;</li>
     8.5  
     8.6  </ul>
     8.7 -
     8.8 -
     9.1 --- a/Admin/page/dist-content/past.content	Mon Sep 11 17:40:41 2000 +0200
     9.2 +++ b/Admin/page/dist-content/past.content	Mon Sep 11 17:41:34 2000 +0200
     9.3 @@ -4,9 +4,10 @@
     9.4  %body%
     9.5  <p> 
     9.6  
     9.7 -The past releases of Isabelle from the Cambrige ftp archive:
     9.8 +Past releases of Isabelle are available from the Cambrige ftp archive:
     9.9  
    9.10  <ul>
    9.11 +<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99.tar.gz">Isabelle99</a> </li>
    9.12  <li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98-1.tar.gz">Isabelle98-1</a> </li>
    9.13  <li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98.tar.gz">Isabelle98</a> </li>
    9.14  <li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-8.tar.gz">Isabelle94-8</a> </li>
    10.1 --- a/Admin/page/dist-content/source.content	Mon Sep 11 17:40:41 2000 +0200
    10.2 +++ b/Admin/page/dist-content/source.content	Mon Sep 11 17:41:34 2000 +0200
    10.3 @@ -2,7 +2,7 @@
    10.4  Isabelle Source Distribution
    10.5  
    10.6  %body%
    10.7 -The standard source distribution of Isabelle:
    10.8 +This is the complete source distribution of <!-- _GP_ distname -->.
    10.9  
   10.10  <p>
   10.11  
   10.12 @@ -11,20 +11,21 @@
   10.13  <center>
   10.14  <table border="0" cellspacing="5" cellpadding="4" width="500">
   10.15  
   10.16 -  <!-- _GP_ download("Isabelle sources with dvi documentation", "{ISABELLE}.tar.gz", "{PACKED_SIZE} K") -->
   10.17 -  <!-- _GP_ download("Documentation as pdf files", "{ISABELLE}_pdf.tar.gz", "{PACKED_SIZE_PDF} K") -->
   10.18 -  <!-- _GP_ download("Browse all files unpacked", "{ISABELLE}", "{UNPACKED_SIZE} K") -->
   10.19 +  <!-- _GP_ download("Isabelle sources with dvi documentation", distname . ".tar.gz", "../..") -->
   10.20 +  <!-- _GP_ download("Documentation as pdf files", distname . "_pdf.tar.gz", "../..") -->
   10.21  
   10.22  </table>
   10.23  </center>
   10.24  
   10.25  <p>
   10.26  
   10.27 -Please see the Isabelle <a href="{ISABELLE}/README.html">README</a>
   10.28 -and <a href="{ISABELLE}/INSTALL">INSTALL</a> files for more
   10.29 -information.
   10.30 +Please see the Isabelle <!-- _GP_ href(distname . "/README.html",
   10.31 +"README") --> and <!-- _GP_ href(distname . "/INSTALL", "INSTALL") -->
   10.32 +files for more information.
   10.33  
   10.34  <p>
   10.35  
   10.36 -Use the mailing list <a href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
   10.37 -to discuss problems and results.  (Why not <A HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?)
   10.38 +Use the mailing list <a
   10.39 +href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
   10.40 +to discuss problems and results.  Why not <a
   10.41 +href="mailto:lcp@cl.cam.ac.uk">subscribe</a>?
    11.1 --- a/Admin/page/dist-layout/navigation.html	Mon Sep 11 17:40:41 2000 +0200
    11.2 +++ b/Admin/page/dist-layout/navigation.html	Mon Sep 11 17:41:34 2000 +0200
    11.3 @@ -1,8 +1,7 @@
    11.4  <p>
    11.5  &nbsp;
    11.6  <center>
    11.7 -<a href="index.html"><img src="{ISABELLE}/lib/logo/isabelle.gif" 
    11.8 -width="100" height="86" alt="[Isabelle logo]" border="0"></a>
    11.9 +<a href="index.html"><img src="isabelle.gif" width="100" height="86" alt="[Isabelle logo]" border="0"></a>
   11.10  </center>
   11.11  <p>
   11.12  <center>
    12.1 --- a/Admin/page/main-content/docs.content	Mon Sep 11 17:40:41 2000 +0200
    12.2 +++ b/Admin/page/main-content/docs.content	Mon Sep 11 17:41:34 2000 +0200
    12.3 @@ -5,4 +5,5 @@
    12.4  
    12.5  <!-- _GP_ include("$pwd/docu-contents.main") -->
    12.6  
    12.7 -All this documentation is also part of the Isabelle <a href="dist/">distribution</a>.
    12.8 +All this documentation is also part of the Isabelle <a
    12.9 +href="dist/">distribution</a> (both as dvi and pdf).
    13.1 --- a/Admin/page/main-content/index.content	Mon Sep 11 17:40:41 2000 +0200
    13.2 +++ b/Admin/page/main-content/index.content	Mon Sep 11 17:41:34 2000 +0200
    13.3 @@ -43,7 +43,7 @@
    13.4    href="dist/source.html">sources</a>, <a
    13.5    href="dist/binary.html">binary packages</a>, and <a
    13.6    href="dist/docs.html">documentation</a>. 
    13.7 -  The current version is <strong>{ISABELLE}</strong>.
    13.8 +  The current version is <strong><!-- _GP_ distname --></strong>.
    13.9  
   13.10  <p>
   13.11  
    14.1 --- a/Admin/page/main-layout/navigation.html	Mon Sep 11 17:40:41 2000 +0200
    14.2 +++ b/Admin/page/main-layout/navigation.html	Mon Sep 11 17:41:34 2000 +0200
    14.3 @@ -1,7 +1,7 @@
    14.4  <p>
    14.5  &nbsp;
    14.6  <center>
    14.7 -<a href="index.html"><img src="dist/{ISABELLE}/lib/logo/isabelle.gif" width="100" height="86" alt="[Isabelle logo]" border="0"></a>
    14.8 +<a href="index.html"><img src="isabelle.gif" width="100" height="86" alt="[Isabelle logo]" border="0"></a>
    14.9  </center>
   14.10  <p>
   14.11  &nbsp;