author | wenzelm |
Fri, 11 Apr 1997 17:30:15 +0200 | |
changeset 2936 | bd33e7aae062 |
parent 2916 | d761a62da697 |
child 2940 | baae674b1d29 |
permissions | -rwxr-xr-x |
2332 | 1 |
#!/bin/bash -norc |
2 |
# |
|
3 |
# $Id$ |
|
4 |
# |
|
5 |
# DESCRIPTION: view Isabelle documentation |
|
6 |
# |
|
7 |
# TODO: |
|
8 |
# - other formats than dvi (??) |
|
9 |
||
10 |
||
11 |
PRG=$(basename $0) |
|
12 |
||
13 |
function usage() |
|
14 |
{ |
|
15 |
echo |
|
16 |
echo "Usage: $PRG [DOC]" |
|
17 |
echo |
|
18 |
echo " View Isabelle documentation DOC, or show list of available documents." |
|
19 |
echo |
|
20 |
exit 1 |
|
21 |
} |
|
22 |
||
23 |
function fail() |
|
24 |
{ |
|
25 |
echo "$1" >&2 |
|
26 |
exit 2 |
|
27 |
} |
|
28 |
||
29 |
||
30 |
## args |
|
31 |
||
32 |
DOC="" |
|
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2916
diff
changeset
|
33 |
[ $# -ge 1 ] && { DOC="$1"; shift; } |
2332 | 34 |
|
35 |
[ $# -ne 0 -o "$DOC" = "-?" ] && usage |
|
36 |
||
37 |
||
38 |
## main |
|
39 |
||
40 |
if [ -z "$DOC" ]; then |
|
41 |
for DIR in $ISABELLE_DOCS |
|
42 |
do |
|
43 |
[ -f $DIR/Contents ] && cat $DIR/Contents |
|
44 |
done |
|
45 |
else |
|
46 |
for DIR in $ISABELLE_DOCS |
|
47 |
do |
|
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2916
diff
changeset
|
48 |
[ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; } |
2332 | 49 |
done |
50 |
fail "Unknown Isabelle document: $DOC" |
|
51 |
fi |