equal
deleted
inserted
replaced
28 |
28 |
29 |
29 |
30 ## args |
30 ## args |
31 |
31 |
32 DOC="" |
32 DOC="" |
33 [ $# -ge 1 ] && { DOC="$1"; shift } |
33 [ $# -ge 1 ] && { DOC="$1"; shift; } |
34 |
34 |
35 [ $# -ne 0 -o "$DOC" = "-?" ] && usage |
35 [ $# -ne 0 -o "$DOC" = "-?" ] && usage |
36 |
36 |
37 |
37 |
38 ## main |
38 ## main |
43 [ -f $DIR/Contents ] && cat $DIR/Contents |
43 [ -f $DIR/Contents ] && cat $DIR/Contents |
44 done |
44 done |
45 else |
45 else |
46 for DIR in $ISABELLE_DOCS |
46 for DIR in $ISABELLE_DOCS |
47 do |
47 do |
48 [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi } |
48 [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; } |
49 done |
49 done |
50 fail "Unknown Isabelle document: $DOC" |
50 fail "Unknown Isabelle document: $DOC" |
51 fi |
51 fi |