lib/Tools/browser
author wenzelm
Tue Jul 04 01:10:53 2000 +0200 (2000-07-04)
changeset 9237 161fb7f00414
parent 9208 7bf28980c521
child 9788 df671fa2562a
permissions -rwxr-xr-x
fixed usage;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # DESCRIPTION: Isabelle graph browser
     6 
     7 
     8 PRG=$(basename $0)
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: $PRG [OPTIONS] [GRAPHFILE]"
    14   echo
    15   echo "  Options are:"
    16   echo "    -d           delete file after use"
    17   echo
    18   exit 1
    19 }
    20 
    21 ## process command line
    22 
    23 # options
    24 
    25 DELETE=""
    26 
    27 while getopts "d" OPT
    28 do
    29   case "$OPT" in
    30     d)
    31       DELETE=true
    32       ;;
    33     \?)
    34       usage
    35       ;;
    36   esac
    37 done
    38 
    39 shift $(($OPTIND - 1))
    40 
    41 
    42 # args
    43 
    44 GRAPHFILE=""
    45 [ $# -gt 0 ] && { GRAPHFILE="$1"; shift; }
    46 [ $# -ne 0 ] && usage
    47 
    48 
    49 ## main
    50 
    51 export CLASSPATH=$ISABELLE_HOME/lib/browser
    52 [ -z "$GRAPHFILE" ] && cd $ISABELLE_BROWSER_INFO
    53 
    54 java GraphBrowser.GraphBrowser $GRAPHFILE
    55 [ -n "$GRAPHFILE" -a -n "$DELETE" ] && rm -f "$GRAPHFILE"