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