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