equal
deleted
inserted
replaced
8 PRG="$(basename "$0")" |
8 PRG="$(basename "$0")" |
9 |
9 |
10 function usage() |
10 function usage() |
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: isabelle $PRG [DOC]" |
13 echo "Usage: isabelle $PRG [DOC ...]" |
14 echo |
14 echo |
15 echo " View Isabelle documentation DOC, or show list of available documents." |
15 echo " View Isabelle documentation." |
16 echo |
16 echo |
17 exit 1 |
17 exit 1 |
18 } |
18 } |
19 |
19 |
20 function fail() |
20 function fail() |
24 } |
24 } |
25 |
25 |
26 |
26 |
27 ## args |
27 ## args |
28 |
28 |
29 DOC="" |
29 [ "$#" -eq 1 -a "$1" = "-?" ] && usage |
30 [ "$#" -ge 1 ] && { DOC="$1"; shift; } |
|
31 |
|
32 [ "$#" -ne 0 -o "$DOC" = "-?" ] && usage |
|
33 |
30 |
34 |
31 |
35 ## main |
32 ## main |
36 |
33 |
37 splitarray ":" "$ISABELLE_DOCS"; DOCS=("${SPLITARRAY[@]}") |
34 isabelle_admin_build jars || exit $? |
38 |
35 |
39 if [ -z "$DOC" ]; then |
36 "$ISABELLE_TOOL" java isabelle.Doc "$@" |
40 for DIR in "${DOCS[@]}" |
|
41 do |
|
42 [ -d "$DIR" ] || fail "Bad documentation directory: \"$DIR\"" |
|
43 [ -f "$DIR/Contents" ] && cat "$DIR/Contents" |
|
44 done |
|
45 else |
|
46 for DIR in "${DOCS[@]}" |
|
47 do |
|
48 [ -d "$DIR" ] || fail "Bad documentation directory: \"$DIR\"" |
|
49 for FMT in "$ISABELLE_DOC_FORMAT" dvi |
|
50 do |
|
51 [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; } |
|
52 done |
|
53 done |
|
54 fail "Missing Isabelle documentation: \"$DOC\"" |
|
55 fi |
|
56 |
37 |