lib/Tools/browser
author wenzelm
Fri Sep 01 19:42:11 2000 +0200 (2000-09-01)
changeset 9794 2be239143d42
parent 9788 df671fa2562a
child 10511 efb3428c9879
permissions -rwxr-xr-x
fixed quoting;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 # Author: Markus Wenzel, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # DESCRIPTION: Isabelle graph browser
     8 
     9 
    10 PRG=$(basename "$0")
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG [OPTIONS] [GRAPHFILE]"
    16   echo
    17   echo "  Options are:"
    18   echo "    -d           delete file after use"
    19   echo
    20   exit 1
    21 }
    22 
    23 ## process command line
    24 
    25 # options
    26 
    27 DELETE=""
    28 
    29 while getopts "d" OPT
    30 do
    31   case "$OPT" in
    32     d)
    33       DELETE=true
    34       ;;
    35     \?)
    36       usage
    37       ;;
    38   esac
    39 done
    40 
    41 shift $(($OPTIND - 1))
    42 
    43 
    44 # args
    45 
    46 GRAPHFILE=""
    47 [ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
    48 [ "$#" -ne 0 ] && usage
    49 
    50 
    51 ## main
    52 
    53 export CLASSPATH="$ISABELLE_HOME/lib/browser"
    54 if [ -z "$GRAPHFILE" ]; then
    55   cd "$ISABELLE_BROWSER_INFO"
    56   exec java GraphBrowser.GraphBrowser
    57 else
    58   java GraphBrowser.GraphBrowser "$GRAPHFILE"
    59   [ -n "$DELETE" ] && rm -f "$GRAPHFILE"
    60 fi
    61