# HG changeset patch
# User gagern
# Date 1173086072 -3600
# Node ID 5f7c9c82b05eaaa3cc1c3cfb59380ffac156ebad
# Parent  3878265f4924434071499f4cbe6c6e9e55e41304
AnnoMaLy related files, as discussed in mails with Gerwin Klein

diff -r 3878265f4924 -r 5f7c9c82b05e Admin/annomaly
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/annomaly	Mon Mar 05 10:14:32 2007 +0100
@@ -0,0 +1,70 @@
+#!/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
+
+ISABELLE_CVS="$(cd "$HOME/isabelle.cvs"; pwd -P)"
+ISABELLE_HOME="$ISABELLE_CVS/Distribution"
+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_REWRITE="isabelle=$ISABELLE_CVS"
+# 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
+
+# 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
+
+# Update CVS
+cd "$ISABELLE_CVS"
+if $CVSUP; then
+  echo "Updating CVS"
+  cvs -q up -d
+fi
+
+# Build isabelle
+cd "$ISABELLE_HOME"
+rm -rf heaps/*
+./build -b $TARGET
+
+# 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 3878265f4924 -r 5f7c9c82b05e Admin/isatest/settings/annomaly
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/settings/annomaly	Mon Mar 05 10:14:32 2007 +0100
@@ -0,0 +1,4 @@
+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")
diff -r 3878265f4924 -r 5f7c9c82b05e src/Pure/ML-Systems/annomaly.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/annomaly.ML	Mon Mar 05 10:14:32 2007 +0100
@@ -0,0 +1,26 @@
+use "ML-Systems/smlnj.ML";                                      
+
+local
+
+  val smlnj_use_text = use_text
+
+  fun strip ([], name, _) = name
+    | strip (["Distribution"], name, _) = name
+    | strip (h1 :: t1, h2 :: t2, def) =
+      if h1 = h2 then strip (t1, t2, def) else def
+
+  fun rewrite (NONE, name) = "use_text" :: name
+    | rewrite (SOME home, name) =
+      strip (#arcs (OS.Path.fromString home), name, "use_text" :: name)
+
+in
+
+  fun use_text name p v t = 
+      let val name = case name of "" => "unnamed" | name => name
+	  val arcs = rewrite (OS.Process.getEnv "ISABELLE_HOME",
+			      #arcs (OS.Path.fromString name))
+	  val _    = AnnoMaLy.nameNextStream ("isabelle" :: arcs)
+      in  smlnj_use_text name p v t
+      end
+
+end;