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