lib/Tools/doc
author wenzelm
Tue Aug 04 15:05:34 2009 +0200 (2009-08-04)
changeset 32322 45cb4a86eca2
parent 29143 72c960b2b83e
child 32390 468eff174a77
permissions -rwxr-xr-x
change IFS only locally -- thanks to bash arrays;
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@2332
     2
#
wenzelm@9788
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm@2332
     4
#
wenzelm@2332
     5
# DESCRIPTION: view Isabelle documentation
wenzelm@2332
     6
wenzelm@2332
     7
wenzelm@10511
     8
PRG="$(basename "$0")"
wenzelm@2332
     9
wenzelm@2332
    10
function usage()
wenzelm@2332
    11
{
wenzelm@2332
    12
  echo
wenzelm@28650
    13
  echo "Usage: isabelle $PRG [DOC]"
wenzelm@2332
    14
  echo
wenzelm@2332
    15
  echo "  View Isabelle documentation DOC, or show list of available documents."
wenzelm@2332
    16
  echo
wenzelm@2332
    17
  exit 1
wenzelm@2332
    18
}
wenzelm@2332
    19
wenzelm@2332
    20
function fail()
wenzelm@2332
    21
{
wenzelm@2332
    22
  echo "$1" >&2
wenzelm@2332
    23
  exit 2
wenzelm@2332
    24
}
wenzelm@2332
    25
wenzelm@2332
    26
wenzelm@2332
    27
## args
wenzelm@2332
    28
wenzelm@2332
    29
DOC=""
wenzelm@9788
    30
[ "$#" -ge 1 ] && { DOC="$1"; shift; }
wenzelm@2332
    31
wenzelm@9788
    32
[ "$#" -ne 0 -o "$DOC" = "-?" ] && usage
wenzelm@2332
    33
wenzelm@2332
    34
wenzelm@2332
    35
## main
wenzelm@2332
    36
wenzelm@32322
    37
ORIG_IFS="$IFS"; IFS=":"; declare -a DOCS=($ISABELLE_DOCS); IFS="$ORIG_IFS"
wenzelm@32322
    38
wenzelm@2332
    39
if [ -z "$DOC" ]; then
wenzelm@32322
    40
  for DIR in "${DOCS[@]}"
wenzelm@2332
    41
  do
wenzelm@15703
    42
    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
wenzelm@9788
    43
    [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
wenzelm@2332
    44
  done
wenzelm@2332
    45
else
wenzelm@32322
    46
  for DIR in "${DOCS[@]}"
wenzelm@2332
    47
  do
wenzelm@15703
    48
    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
wenzelm@15703
    49
    for FMT in "$ISABELLE_DOC_FORMAT" dvi
wenzelm@15703
    50
    do
wenzelm@28500
    51
      [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
wenzelm@15703
    52
    done
wenzelm@2332
    53
  done
wenzelm@2332
    54
  fail "Unknown Isabelle document: $DOC"  
wenzelm@2332
    55
fi
wenzelm@15717
    56