# HG changeset patch
# User wenzelm
# Date 1343045908 -7200
# Node ID c8c7b2b388d1851834f5e834d0789dbed3bd08e0
# Parent  6f2762eedca0f4e99f18849af3b160d96351e506
removed some old/unused stuff;

diff -r 6f2762eedca0 -r c8c7b2b388d1 Admin/isatest/annomaly
--- a/Admin/isatest/annomaly	Mon Jul 23 12:05:48 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,98 +0,0 @@
-#!/bin/sh
-
-# Create AnnoMaLy documentation for Isabelle
-# See http://martin.von-gagern.net/projects/annomaly/
-#   2007  Martin von Gagern (martin@von-gagern.net)
-
-# Abort on any error
-set -e -o pipefail
-
-BUILD_DIR="$HOME/isabelle.annomaly"
-ISABELLE_HOME="$BUILD_DIR/Isabelle"
-ISABELLE_CVS="$HOME/isabelle.cvs"
-ADMIN_CVS="$ISABELLE_CVS/Admin"
-# ISABELLE_HOME="$ISABELLE_CVS/Distribution"
-ISABELLE_SRC="$ISABELLE_HOME/src"
-HTML_DIR="$HOME/html-data/isabelle-doc"
-export CVS_RSH=ssh
-export SMLNJ_HOME="$HOME/annomaly"
-export PATH="$SMLNJ_HOME/bin:$PATH"
-export SML_DOC_DIR="$HTML_DIR.tmp"
-# export SML_DOC_DEBUG="all"
-TARGET=HOL
-CVSUP=true
-
-# Parse command line
-for ARG in "$@"; do case "$ARG" in
-	-p) TARGET=Pure ;;
-	-n) CVSUP=false ;;
-	-l) export SML_LOG_DIR="$HOME/logs" ;;
-esac; done
-
-# Update CVS
-cd "$ADMIN_CVS"
-if $CVSUP; then
-  echo "Updating CVS"
-  cvs -q up -d
-fi
-
-# Find nightly isabelle tarball
-ISABELLE_TAR=""
-for i in /home/html/isatest/Isabelle_[0-9]*-20[0-9][0-9].tar.gz; do
-  if [[ -r "$i" ]]; then ISABELLE_TAR="$i"; fi
-done
-if [[ -z $ISABELLE_TAR ]]; then
-  echo "No isabelle tarball found!" >&2
-  exit 1
-fi
-
-# Create build environemnt
-mkdir -p "$BUILD_DIR"
-cd "$BUILD_DIR"
-if [[ -d Isabelle ]]; then
-  rm -rf *
-fi
-tar xzf "$ISABELLE_TAR"
-cd "$ISABELLE_HOME"
-cp "$ADMIN_CVS"/isatest/annomaly.ML src/Pure/ML-Systems/annomaly.ML
-ln -s run-smlnj lib/scripts/run-annomaly
-
-# 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
-
-# Build isabelle
-ISABELLE_HOME="$(cd "$ISABELLE_HOME"; pwd -P)"
-cd "$ISABELLE_HOME"
-export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
-rm -rf heaps
-./build -b $TARGET
-cd "$BUILD_DIR"
-rm -rf *
-
-# 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
-grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
-
-# Install result by renaming, to be almost atomic
-rm -rf "$HTML_DIR.bac"
-if [[ -d $HTML_DIR ]]; then mv "$HTML_DIR" "$HTML_DIR.bac"; fi
-mv "$SML_DOC_DIR" "$HTML_DIR"
-rm -rf "$HTML_DIR.bac"
-
-# Done
-echo "Completed successfully"
-exit 0
diff -r 6f2762eedca0 -r c8c7b2b388d1 Admin/isatest/annomaly.ML
--- a/Admin/isatest/annomaly.ML	Mon Jul 23 12:05:48 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(*  Title:      Admin/isatest/annomaly.ML
-    Author:     Martin von Gagern <martin@von-gagern.net>
-*)
-
-use "ML-Systems/smlnj.ML";
-
-local
-
-  val smlnj_use_text = use_text
-
-  val smlnj_use_file = use_file
-
-  val smlnj_forget_structure = forget_structure
-
-  fun mkAbsolute path =
-      OS.Path.mkAbsolute { path = path, relativeTo = OS.FileSys.getDir () }
-
-  fun toArcs path = #arcs (OS.Path.fromString path)
-
-  val isabelleHome =
-      case OS.Process.getEnv "ISABELLE_HOME"
-       of  NONE => OS.FileSys.getDir ()
-         | SOME home => mkAbsolute home
-
-  fun noparent [] = []
-    | noparent (n :: ns) =
-      if n = OS.Path.parentArc then noparent ns else n :: noparent ns
-
-  fun isabellePath [] = []
-    | isabellePath ("src" :: name) = "Isabelle" :: name
-    | isabellePath (name as (n :: ns)) =
-      if n = OS.Path.parentArc then noparent ns else "Isabelle" :: name
-
-  fun rewrite defPrefix name =
-      let val abs = mkAbsolute name
-          val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
-          val exists = (OS.FileSys.access(abs, nil)
-                        handle OS.SysErr _ => false)
-      in  if exists andalso rel <> ""
-          then isabellePath (toArcs rel)
-          else defPrefix @ noparent (toArcs name)
-      end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
-
-in
-
-  fun use_text tune str_of_pos name_space (line, name) p v t =
-    let val name = case name of "" => "unnamed" | name => name
-        val arcs = rewrite ["use_text"] name
-        (* should we have different files for different line numbers? *
-        val arcs = if line <= 1 then arcs
-                   else arcs @ [ "l." ^ Int.toString line ]
-        *)
-        val arcs = if t = "structure Isabelle =\nstruct\nend;"
-                      andalso name = "ML"
-                   then ["empty_Isabelle", "empty" ] else arcs
-        val _    = AnnoMaLy.nameNextStream arcs
-    in  smlnj_use_text tune str_of_pos name_space (line, name) p v t  end;
-
-  fun use_file tune str_of_pos name_space output verbose name =
-      let val arcs = rewrite ["use_file"] name
-          val _    = AnnoMaLy.nameNextStream arcs
-      in  smlnj_use_file tune str_of_pos name_space output verbose name  end;
-
-  fun forget_structure name =
-      let val arcs = [ "forget_structure", name ]
-          val _    = AnnoMaLy.nameNextStream arcs
-      in  smlnj_forget_structure name  end;
-
-end;
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."
diff -r 6f2762eedca0 -r c8c7b2b388d1 Admin/isatest/settings/annomaly
--- a/Admin/isatest/settings/annomaly	Mon Jul 23 12:05:48 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-ML_SYSTEM=annomaly
-ML_HOME="$SMLNJ_HOME/bin"
-ML_OPTIONS="-m $SMLNJ_HOME/annomaly/annomaly.cm @SMLdebug=/dev/null"
-ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-
-
-ISABELLE_HOME_USER="$HOME/isabelle-annomaly"
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
-