lib/Tools/doc
author paulson
Tue, 10 Feb 2004 12:02:11 +0100
changeset 14378 69c4d5997669
parent 10555 2323ec838401
child 14981 e73f8140af78
permissions -rwxr-xr-x
generic of_nat and of_int functions, and generalization of iszero and neg
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10511
diff changeset
     1
#!/usr/bin/env bash
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
     2
#
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
     3
# $Id$
9788
wenzelm
parents: 8130
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 8130
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
     6
#
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
     7
# DESCRIPTION: view Isabelle documentation
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
     8
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
     9
10511
wenzelm
parents: 9788
diff changeset
    10
PRG="$(basename "$0")"
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    11
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    12
function usage()
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    13
{
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    14
  echo
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    15
  echo "Usage: $PRG [DOC]"
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    16
  echo
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    17
  echo "  View Isabelle documentation DOC, or show list of available documents."
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    18
  echo
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    19
  exit 1
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    20
}
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    21
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    22
function fail()
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    23
{
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    24
  echo "$1" >&2
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    25
  exit 2
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    26
}
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    27
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    28
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    29
## args
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    30
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    31
DOC=""
9788
wenzelm
parents: 8130
diff changeset
    32
[ "$#" -ge 1 ] && { DOC="$1"; shift; }
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    33
9788
wenzelm
parents: 8130
diff changeset
    34
[ "$#" -ne 0 -o "$DOC" = "-?" ] && usage
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    35
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    36
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    37
## main
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    38
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    39
if [ -z "$DOC" ]; then
9788
wenzelm
parents: 8130
diff changeset
    40
  ORIG_IFS="$IFS"
wenzelm
parents: 8130
diff changeset
    41
  IFS=":"
wenzelm
parents: 8130
diff changeset
    42
  for DIR in $ISABELLE_DOCS
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    43
  do
9788
wenzelm
parents: 8130
diff changeset
    44
    [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    45
  done
9788
wenzelm
parents: 8130
diff changeset
    46
  IFS="$ORIG_IFS"
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    47
else
9788
wenzelm
parents: 8130
diff changeset
    48
  ORIG_IFS="$IFS"
wenzelm
parents: 8130
diff changeset
    49
  IFS=":"
wenzelm
parents: 8130
diff changeset
    50
  for DIR in $ISABELLE_DOCS
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    51
  do
9788
wenzelm
parents: 8130
diff changeset
    52
    [ -f "$DIR/$DOC.dvi" ] && { cd "$DIR"; IFS="$ORIG_IFS"; exec $DVI_VIEWER "$DOC.dvi"; }
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    53
  done
9788
wenzelm
parents: 8130
diff changeset
    54
  IFS="$ORIG_IFS"
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    55
  fail "Unknown Isabelle document: $DOC"  
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    56
fi