lib/Tools/doc
author wenzelm
Wed, 15 Apr 2009 11:14:48 +0200
changeset 30895 bad26d8f0adf
parent 29143 72c960b2b83e
child 32322 45cb4a86eca2
permissions -rwxr-xr-x
updated for Isabelle2009;
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
#
9788
wenzelm
parents: 8130
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
     4
#
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: view Isabelle documentation
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
     6
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
     7
10511
wenzelm
parents: 9788
diff changeset
     8
PRG="$(basename "$0")"
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
     9
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    10
function usage()
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    11
{
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    12
  echo
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 28500
diff changeset
    13
  echo "Usage: isabelle $PRG [DOC]"
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    14
  echo
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    15
  echo "  View Isabelle documentation DOC, or show list of available documents."
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    16
  echo
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    17
  exit 1
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    18
}
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    19
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    20
function fail()
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    21
{
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    22
  echo "$1" >&2
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    23
  exit 2
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    24
}
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    25
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    26
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    27
## args
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    28
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    29
DOC=""
9788
wenzelm
parents: 8130
diff changeset
    30
[ "$#" -ge 1 ] && { DOC="$1"; shift; }
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    31
9788
wenzelm
parents: 8130
diff changeset
    32
[ "$#" -ne 0 -o "$DOC" = "-?" ] && usage
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    33
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    34
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    35
## main
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    36
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    37
if [ -z "$DOC" ]; then
9788
wenzelm
parents: 8130
diff changeset
    38
  ORIG_IFS="$IFS"
wenzelm
parents: 8130
diff changeset
    39
  IFS=":"
wenzelm
parents: 8130
diff changeset
    40
  for DIR in $ISABELLE_DOCS
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    41
  do
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 14981
diff changeset
    42
    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
9788
wenzelm
parents: 8130
diff changeset
    43
    [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    44
  done
9788
wenzelm
parents: 8130
diff changeset
    45
  IFS="$ORIG_IFS"
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    46
else
9788
wenzelm
parents: 8130
diff changeset
    47
  ORIG_IFS="$IFS"
wenzelm
parents: 8130
diff changeset
    48
  IFS=":"
wenzelm
parents: 8130
diff changeset
    49
  for DIR in $ISABELLE_DOCS
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    50
  do
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 14981
diff changeset
    51
    IFS="$ORIG_IFS"
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 14981
diff changeset
    52
    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 14981
diff changeset
    53
    for FMT in "$ISABELLE_DOC_FORMAT" dvi
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 14981
diff changeset
    54
    do
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 15717
diff changeset
    55
      [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 14981
diff changeset
    56
    done
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    57
  done
9788
wenzelm
parents: 8130
diff changeset
    58
  IFS="$ORIG_IFS"
2332
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    59
  fail "Unknown Isabelle document: $DOC"  
ae592411c199 doc: view Isabelle documentation;
wenzelm
parents:
diff changeset
    60
fi
15717
541e50adfc73 *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm
parents: 15703
diff changeset
    61