Admin/isatest/isatest-annomaly
changeset 48444 c8c7b2b388d1
parent 48443 6f2762eedca0
child 48445 cb4136e4cabf
equal deleted inserted replaced
48443:6f2762eedca0 48444:c8c7b2b388d1
     1 #!/usr/bin/env bash
       
     2 #
       
     3 # Create AnnoMaLy documentation for Isabelle
       
     4 #
       
     5 # Based on http://martin.von-gagern.net/projects/annomaly/
       
     6 #   2007  Martin von Gagern (martin@von-gagern.net)
       
     7 
       
     8 ## global settings
       
     9 . ~/admin/isatest/isatest-settings
       
    10 
       
    11 PRG="$(basename "$0")"
       
    12 
       
    13 export SMLNJ_HOME="/home/gagern/annomaly"
       
    14 export SML_DOC_DIR="$HOME/anno-html"
       
    15 
       
    16 ADMIN="$HOME/admin/isatest"
       
    17 LOGICS="HOL"
       
    18 
       
    19 # Abort on any error
       
    20 set -e -o pipefail
       
    21 
       
    22 function usage()
       
    23 {
       
    24   echo
       
    25   echo "Usage: $PRG"
       
    26   echo
       
    27   echo "  Generate html documentation from .ML files"
       
    28   echo
       
    29   exit 1
       
    30 }
       
    31 
       
    32 function fail()
       
    33 {
       
    34   echo "$1" >&2
       
    35   log "FAILED, $1"
       
    36   exit 2
       
    37 }
       
    38 
       
    39 
       
    40 ## main
       
    41 
       
    42 ISABELLE_HOME="$DISTPREFIX/Isabelle"
       
    43 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
       
    44 
       
    45 [ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
       
    46 
       
    47 
       
    48 # Create clean output directory
       
    49 rm -rf "$SML_DOC_DIR"
       
    50 mkdir "$SML_DOC_DIR"
       
    51 cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
       
    52 cat > "$SML_DOC_DIR/.htaccess" <<EOF
       
    53 DirectoryIndex index.html source.html
       
    54 <IfModule mod_deflate>
       
    55 SetOutputFilter DEFLATE 
       
    56 </IfModule>
       
    57 AddType text/plain .dot
       
    58 EOF
       
    59 
       
    60 # Prepare build environemnt
       
    61 cd "$ISABELLE_HOME"
       
    62 cp "$ADMIN/annomaly.ML" src/Pure/ML-Systems/annomaly.ML
       
    63 ln -fs run-smlnj lib/scripts/run-annomaly
       
    64 
       
    65 cd "$ISABELLE_HOME"
       
    66 export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
       
    67 
       
    68 
       
    69 # Process image(s)
       
    70 for L in $LOGICS
       
    71 do
       
    72   ( cd "$ISABELLE_HOME/src/$L"; \
       
    73     cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
       
    74     "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
       
    75 done
       
    76 
       
    77 
       
    78 # Postprocess created files
       
    79 cd "$SML_DOC_DIR"
       
    80 dot -Tsvg depGraph.dot \
       
    81   | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
       
    82   > depGraph.svg
       
    83 dot -Tps2 depGraph.dot > depGraph.ps
       
    84 ps2pdf depGraph.ps depGraph.pdf
       
    85 
       
    86 # $ISABELLE_HOME does not seem to occur anywhere ??
       
    87 # grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
       
    88 
       
    89 
       
    90 log "annomaly docs generated successfully."