lib/Tools/doc
author wenzelm
Fri Sep 01 17:50:36 2000 +0200 (2000-09-01)
changeset 9788 df671fa2562a
parent 8130 b077b79061b6
child 10511 efb3428c9879
permissions -rwxr-xr-x
GPLed;
more robust handling of spaces in args / file names;
wenzelm@3007
     1
#!/bin/bash
wenzelm@2332
     2
#
wenzelm@2332
     3
# $Id$
wenzelm@9788
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@9788
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@2332
     6
#
wenzelm@2332
     7
# DESCRIPTION: view Isabelle documentation
wenzelm@2332
     8
wenzelm@2332
     9
wenzelm@9788
    10
PRG=$(basename "$0")
wenzelm@2332
    11
wenzelm@2332
    12
function usage()
wenzelm@2332
    13
{
wenzelm@2332
    14
  echo
wenzelm@2332
    15
  echo "Usage: $PRG [DOC]"
wenzelm@2332
    16
  echo
wenzelm@2332
    17
  echo "  View Isabelle documentation DOC, or show list of available documents."
wenzelm@2332
    18
  echo
wenzelm@2332
    19
  exit 1
wenzelm@2332
    20
}
wenzelm@2332
    21
wenzelm@2332
    22
function fail()
wenzelm@2332
    23
{
wenzelm@2332
    24
  echo "$1" >&2
wenzelm@2332
    25
  exit 2
wenzelm@2332
    26
}
wenzelm@2332
    27
wenzelm@2332
    28
wenzelm@2332
    29
## args
wenzelm@2332
    30
wenzelm@2332
    31
DOC=""
wenzelm@9788
    32
[ "$#" -ge 1 ] && { DOC="$1"; shift; }
wenzelm@2332
    33
wenzelm@9788
    34
[ "$#" -ne 0 -o "$DOC" = "-?" ] && usage
wenzelm@2332
    35
wenzelm@2332
    36
wenzelm@2332
    37
## main
wenzelm@2332
    38
wenzelm@2332
    39
if [ -z "$DOC" ]; then
wenzelm@9788
    40
  ORIG_IFS="$IFS"
wenzelm@9788
    41
  IFS=":"
wenzelm@9788
    42
  for DIR in $ISABELLE_DOCS
wenzelm@2332
    43
  do
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@9788
    52
    [ -f "$DIR/$DOC.dvi" ] && { cd "$DIR"; IFS="$ORIG_IFS"; exec $DVI_VIEWER "$DOC.dvi"; }
wenzelm@2332
    53
  done
wenzelm@9788
    54
  IFS="$ORIG_IFS"
wenzelm@2332
    55
  fail "Unknown Isabelle document: $DOC"  
wenzelm@2332
    56
fi