equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
|
4 # Author: Markus Wenzel, TU Muenchen |
|
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 # |
6 # |
5 # DESCRIPTION: Isabelle graph browser |
7 # DESCRIPTION: Isabelle graph browser |
6 |
8 |
7 |
9 |
8 PRG=$(basename $0) |
10 PRG=$(basename "$0") |
9 |
11 |
10 function usage() |
12 function usage() |
11 { |
13 { |
12 echo |
14 echo |
13 echo "Usage: $PRG [OPTIONS] [GRAPHFILE]" |
15 echo "Usage: $PRG [OPTIONS] [GRAPHFILE]" |
40 |
42 |
41 |
43 |
42 # args |
44 # args |
43 |
45 |
44 GRAPHFILE="" |
46 GRAPHFILE="" |
45 [ $# -gt 0 ] && { GRAPHFILE="$1"; shift; } |
47 [ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; } |
46 [ $# -ne 0 ] && usage |
48 [ "$#" -ne 0 ] && usage |
47 |
49 |
48 |
50 |
49 ## main |
51 ## main |
50 |
52 |
51 export CLASSPATH=$ISABELLE_HOME/lib/browser |
53 export CLASSPATH="$ISABELLE_HOME/lib/browser" |
52 [ -z "$GRAPHFILE" ] && cd $ISABELLE_BROWSER_INFO |
54 [ -z "$GRAPHFILE" ] && cd "$ISABELLE_BROWSER_INFO" |
53 |
55 |
54 java GraphBrowser.GraphBrowser $GRAPHFILE |
56 java GraphBrowser.GraphBrowser "$GRAPHFILE" |
55 [ -n "$GRAPHFILE" -a -n "$DELETE" ] && rm -f "$GRAPHFILE" |
57 [ -n "$GRAPHFILE" -a -n "$DELETE" ] && rm -f "$GRAPHFILE" |