isatest version of annomaly script. to be run from istatest-makedist.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-annomaly	Thu Apr 12 02:42:58 2007 +0200
@@ -0,0 +1,92 @@
+#!/usr/bin/env bash
+#
+# $Id$
+#
+# Create AnnoMaLy documentation for Isabelle
+#
+# Based on http://martin.von-gagern.net/projects/annomaly/
+#   2007  Martin von Gagern ([e-mail])
+
+## 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
+  echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
+  exit 2
+}
+
+
+## main
+
+ISABELLE_HOME="$DISTPREFIX/Isabelle"
+ISATOOL="$ISABELLE_HOME/bin/isatool"
+
+[ -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; \
+    "$ISATOOL" make || fail "isatool 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"
+
+
+echo "$(date) $HOSTNAME $PRG: annomaly docs generated successfully." >> $MASTERLOG