diff -r 6f2762eedca0 -r c8c7b2b388d1 Admin/isatest/isatest-annomaly
--- a/Admin/isatest/isatest-annomaly	Mon Jul 23 12:05:48 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-#!/usr/bin/env bash
-#
-# Create AnnoMaLy documentation for Isabelle
-#
-# Based on http://martin.von-gagern.net/projects/annomaly/
-#   2007  Martin von Gagern (martin@von-gagern.net)
-
-## global settings
-. ~/admin/isatest/isatest-settings
-
-PRG="$(basename "$0")"
-
-export SMLNJ_HOME="/home/gagern/annomaly"
-export SML_DOC_DIR="$HOME/anno-html"
-
-ADMIN="$HOME/admin/isatest"
-LOGICS="HOL"
-
-# Abort on any error
-set -e -o pipefail
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG"
-  echo
-  echo "  Generate html documentation from .ML files"
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  log "FAILED, $1"
-  exit 2
-}
-
-
-## main
-
-ISABELLE_HOME="$DISTPREFIX/Isabelle"
-ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
-
-[ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
-
-
-# Create clean output directory
-rm -rf "$SML_DOC_DIR"
-mkdir "$SML_DOC_DIR"
-cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
-cat > "$SML_DOC_DIR/.htaccess" <<EOF
-DirectoryIndex index.html source.html
-<IfModule mod_deflate>
-SetOutputFilter DEFLATE 
-</IfModule>
-AddType text/plain .dot
-EOF
-
-# Prepare build environemnt
-cd "$ISABELLE_HOME"
-cp "$ADMIN/annomaly.ML" src/Pure/ML-Systems/annomaly.ML
-ln -fs run-smlnj lib/scripts/run-annomaly
-
-cd "$ISABELLE_HOME"
-export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
-
-
-# Process image(s)
-for L in $LOGICS
-do
-  ( cd "$ISABELLE_HOME/src/$L"; \
-    cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
-    "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
-done
-
-
-# Postprocess created files
-cd "$SML_DOC_DIR"
-dot -Tsvg depGraph.dot \
-  | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
-  > depGraph.svg
-dot -Tps2 depGraph.dot > depGraph.ps
-ps2pdf depGraph.ps depGraph.pdf
-
-# $ISABELLE_HOME does not seem to occur anywhere ??
-# grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
-
-
-log "annomaly docs generated successfully."