Admin/makepage

use HOLogic.Not;
export indexify_names;

#!/bin/bash
#
# $Id$
#
# makemainpage -- make main Isabelle web pages

TARGET=/usr/proj/isabelle-repository/www
FILES="index.html docs.html about.html cambridge.gif munich.gif"
PREFIX=main

PRG=$(basename $0)
THIS=$(cd $(dirname "$0"); echo $PWD)

function usage()
{
  echo
  echo "Usage: $PRG VERSION DIST"
  echo
  cat <<EOF
  Make Isabelle main web pages with links to documentation for VERSION

  VERSION should be the Isabelle version contained in DIST
  DIST should be an Isabelle distribution archive or directory

EOF
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

[ $# -ne 2 ] && usage

export DISTNAME=$1
shift
DIST=$1

cd $THIS/page

if [ -d $DIST ]; then
    cp $DIST/doc/Contents .
else
  if [ -f $DIST ]; then
      gzip -dc $DIST | tar -Bxf - $DISTNAME/doc/Contents 
      mv $DISTNAME/doc/Contents .
      rmdir -p $DISTNAME/doc
  else 
      echo error: $DIST not found
      fail
  fi
fi

make main

for FILE in $FILES; do
    cp -f $PREFIX/$FILE $TARGET
done

chmod g=u $TARGET/*

( cd $TARGET; echo -e "\nYou should find the Isabelle pages in $PWD"; )