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