lib/Tools/browser
author wenzelm
Thu, 04 Jun 2009 17:31:38 +0200
changeset 31427 5a07cc86675d
parent 29143 72c960b2b83e
child 34283 7911e83d06c0
permissions -rwxr-xr-x
reraise exceptions to preserve original position (ML system specific);
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
#
9788
wenzelm
parents: 9237
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
     4
#
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
     5
# DESCRIPTION: Isabelle graph browser
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
     6
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
     7
10511
wenzelm
parents: 9794
diff changeset
     8
PRG="$(basename "$0")"
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
     9
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    10
function usage()
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    11
{
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    12
  echo
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 28500
diff changeset
    13
  echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]"
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    14
  echo
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    15
  echo "  Options are:"
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    16
  echo "    -c           cleanup -- remove GRAPHFILE after use"
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    17
  echo "    -o FILE      output to FILE (ps, eps, pdf)"
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    18
  echo
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    19
  exit 1
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    20
}
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    21
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    22
function fail()
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    23
{
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    24
  echo "$1" >&2
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    25
  exit 2
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    26
}
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
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    29
## process command line
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    30
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    31
# options
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    32
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    33
CLEAN=""
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    34
OUTFILE=""
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    35
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    36
while getopts "co:" OPT
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    37
do
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    38
  case "$OPT" in
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    39
    c)
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    40
      CLEAN=true
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    41
      ;;
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    42
    o)
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    43
      OUTFILE="$OPTARG"
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    44
      ;;
7766
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
      usage
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    47
      ;;
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    48
  esac
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    49
done
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    50
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    51
shift $(($OPTIND - 1))
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    52
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
# args
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    55
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    56
GRAPHFILE=""
9788
wenzelm
parents: 9237
diff changeset
    57
[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
wenzelm
parents: 9237
diff changeset
    58
[ "$#" -ne 0 ] && usage
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    59
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    60
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    61
## main
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    62
27907
5b9bc956cec6 refined JVM path wrappers;
wenzelm
parents: 26230
diff changeset
    63
classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
25650
ce061f5083d7 added javapath (for cygwin);
wenzelm
parents: 20569
diff changeset
    64
9794
2be239143d42 fixed quoting;
wenzelm
parents: 9788
diff changeset
    65
if [ -z "$GRAPHFILE" ]; then
26230
ba4f5954843d check ISABELLE_BROWSER_INFO before cd;
wenzelm
parents: 25650
diff changeset
    66
  [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 27914
diff changeset
    67
  exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
9794
2be239143d42 fixed quoting;
wenzelm
parents: 9788
diff changeset
    68
else
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    69
  PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    70
  if [ -n "$CLEAN" ]; then
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    71
    mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    72
  else
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    73
    cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $FILE"
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    74
  fi
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    75
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    76
  PDF=""
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    77
  case "$OUTFILE" in
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    78
    *.pdf)
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    79
      OUTFILE="${OUTFILE%%.pdf}.eps"
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    80
      PDF=true
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    81
      ;;
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    82
  esac
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    83
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    84
  if [ -z "$OUTFILE" ]; then
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 27914
diff changeset
    85
    "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")"
11813
berghofe
parents: 11801
diff changeset
    86
  else
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 27914
diff changeset
    87
    "$ISABELLE_TOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")"
11813
berghofe
parents: 11801
diff changeset
    88
  fi
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    89
  RC="$?"
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    90
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    91
  if [ -n "$PDF" ]; then
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    92
    "$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
    93
  fi
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    94
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    95
  rm -f "$PRIVATE_FILE"
9794
2be239143d42 fixed quoting;
wenzelm
parents: 9788
diff changeset
    96
fi
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    97
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    98
exit "$RC"