lib/Tools/browser
author wenzelm
Tue, 13 Jun 2006 23:41:39 +0200
changeset 19876 11d447d5d68c
parent 14981 e73f8140af78
child 20569 c315ba088073
permissions -rwxr-xr-x
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10511
diff changeset
     1
#!/usr/bin/env bash
3640
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
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
     5
#
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
     6
# DESCRIPTION: Isabelle graph browser
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
     7
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
     8
10511
wenzelm
parents: 9794
diff changeset
     9
PRG="$(basename "$0")"
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    10
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    11
function usage()
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    12
{
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    13
  echo
9237
161fb7f00414 fixed usage;
wenzelm
parents: 9208
diff changeset
    14
  echo "Usage: $PRG [OPTIONS] [GRAPHFILE]"
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    15
  echo
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    16
  echo "  Options are:"
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    17
  echo "    -d           delete file after use"
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    18
  echo "    -o FILE      output to FILE (ps, eps, pdf)"
7766
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
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    23
function fail()
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    24
{
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    25
  echo "$1" >&2
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    26
  exit 2
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    27
}
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    28
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    29
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    30
## process command line
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    31
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    32
# options
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    33
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    34
DELETE=""
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    35
OUTFILE=""
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    36
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    37
while getopts "do:" OPT
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    38
do
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    39
  case "$OPT" in
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    40
    d)
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    41
      DELETE=true
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    42
      ;;
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    43
    o)
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    44
      OUTFILE="$OPTARG"
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    45
      ;;
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    46
    \?)
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    47
      usage
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    48
      ;;
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    49
  esac
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    50
done
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    51
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    52
shift $(($OPTIND - 1))
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    53
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    54
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    55
# args
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    56
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    57
GRAPHFILE=""
9788
wenzelm
parents: 9237
diff changeset
    58
[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
wenzelm
parents: 9237
diff changeset
    59
[ "$#" -ne 0 ] && usage
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    60
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    61
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    62
## main
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    63
14546
8c846773878a use .jar
kleing
parents: 13974
diff changeset
    64
export CLASSPATH="$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
9794
2be239143d42 fixed quoting;
wenzelm
parents: 9788
diff changeset
    65
if [ -z "$GRAPHFILE" ]; then
2be239143d42 fixed quoting;
wenzelm
parents: 9788
diff changeset
    66
  cd "$ISABELLE_BROWSER_INFO"
2be239143d42 fixed quoting;
wenzelm
parents: 9788
diff changeset
    67
  exec java GraphBrowser.GraphBrowser
2be239143d42 fixed quoting;
wenzelm
parents: 9788
diff changeset
    68
else
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    69
  PDF=""
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    70
  case "$OUTFILE" in
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    71
    *.pdf)
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    72
      OUTFILE="${OUTFILE%%.pdf}.eps"
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    73
      PDF=true
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    74
      ;;
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    75
  esac
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    76
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    77
  if [ -z "$OUTFILE" ]; then
11813
berghofe
parents: 11801
diff changeset
    78
    java GraphBrowser.GraphBrowser "$GRAPHFILE"
berghofe
parents: 11801
diff changeset
    79
  else
13974
9a4cb68e3315 use different main class for batch mode
kleing
parents: 11900
diff changeset
    80
    java GraphBrowser.Console "$GRAPHFILE" "$OUTFILE"
11813
berghofe
parents: 11801
diff changeset
    81
  fi
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    82
  RC="$?"
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    83
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    84
  if [ -n "$PDF" ]; then
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    85
    "$ISABELLE_EPSTOPDF" "$OUTFILE" || fail "Failed to produce pdf output"
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    86
  fi
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    87
9794
2be239143d42 fixed quoting;
wenzelm
parents: 9788
diff changeset
    88
  [ -n "$DELETE" ] && rm -f "$GRAPHFILE"
2be239143d42 fixed quoting;
wenzelm
parents: 9788
diff changeset
    89
fi
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    90
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    91
exit "$RC"