lib/Tools/browser
author wenzelm
Sat Oct 04 16:05:09 2008 +0200 (2008-10-04 ago)
changeset 28500 4b79e5d3d0aa
parent 27914 9a7f17370ffb
child 28650 a7ba12e0d3b7
permissions -rwxr-xr-x
replaced ISATOOL by ISABELLE_TOOL;
wenzelm@10555
     1
#!/usr/bin/env bash
berghofe@3640
     2
#
berghofe@3640
     3
# $Id$
wenzelm@9788
     4
# Author: Markus Wenzel, TU Muenchen
berghofe@3640
     5
#
berghofe@7766
     6
# DESCRIPTION: Isabelle graph browser
berghofe@3640
     7
berghofe@3640
     8
wenzelm@10511
     9
PRG="$(basename "$0")"
berghofe@3640
    10
berghofe@3640
    11
function usage()
berghofe@3640
    12
{
berghofe@3640
    13
  echo
wenzelm@9237
    14
  echo "Usage: $PRG [OPTIONS] [GRAPHFILE]"
berghofe@3640
    15
  echo
berghofe@7766
    16
  echo "  Options are:"
wenzelm@20569
    17
  echo "    -c           cleanup -- remove GRAPHFILE after use"
wenzelm@11801
    18
  echo "    -o FILE      output to FILE (ps, eps, pdf)"
berghofe@7766
    19
  echo
berghofe@3640
    20
  exit 1
berghofe@3640
    21
}
berghofe@3640
    22
wenzelm@11801
    23
function fail()
wenzelm@11801
    24
{
wenzelm@11801
    25
  echo "$1" >&2
wenzelm@11801
    26
  exit 2
wenzelm@11801
    27
}
wenzelm@11801
    28
wenzelm@11801
    29
berghofe@7766
    30
## process command line
berghofe@7766
    31
berghofe@7766
    32
# options
berghofe@7766
    33
wenzelm@20569
    34
CLEAN=""
wenzelm@11801
    35
OUTFILE=""
berghofe@7766
    36
wenzelm@20569
    37
while getopts "co:" OPT
berghofe@7766
    38
do
berghofe@7766
    39
  case "$OPT" in
wenzelm@20569
    40
    c)
wenzelm@20569
    41
      CLEAN=true
berghofe@7766
    42
      ;;
wenzelm@11801
    43
    o)
wenzelm@11801
    44
      OUTFILE="$OPTARG"
wenzelm@11801
    45
      ;;
berghofe@7766
    46
    \?)
berghofe@7766
    47
      usage
berghofe@7766
    48
      ;;
berghofe@7766
    49
  esac
berghofe@7766
    50
done
berghofe@7766
    51
berghofe@7766
    52
shift $(($OPTIND - 1))
berghofe@7766
    53
berghofe@7766
    54
berghofe@7766
    55
# args
berghofe@7766
    56
berghofe@7766
    57
GRAPHFILE=""
wenzelm@9788
    58
[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
wenzelm@9788
    59
[ "$#" -ne 0 ] && usage
berghofe@7766
    60
berghofe@3640
    61
berghofe@3640
    62
## main
berghofe@3640
    63
wenzelm@27907
    64
classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
wenzelm@25650
    65
wenzelm@9794
    66
if [ -z "$GRAPHFILE" ]; then
wenzelm@26230
    67
  [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
wenzelm@28500
    68
  exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
wenzelm@9794
    69
else
wenzelm@20569
    70
  PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
wenzelm@20569
    71
  if [ -n "$CLEAN" ]; then
wenzelm@20569
    72
    mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
wenzelm@20569
    73
  else
wenzelm@20569
    74
    cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $FILE"
wenzelm@20569
    75
  fi
wenzelm@20569
    76
wenzelm@11843
    77
  PDF=""
wenzelm@11801
    78
  case "$OUTFILE" in
wenzelm@11801
    79
    *.pdf)
wenzelm@11843
    80
      OUTFILE="${OUTFILE%%.pdf}.eps"
wenzelm@11801
    81
      PDF=true
wenzelm@11801
    82
      ;;
wenzelm@11801
    83
  esac
wenzelm@11801
    84
wenzelm@11843
    85
  if [ -z "$OUTFILE" ]; then
wenzelm@28500
    86
    "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")"
berghofe@11813
    87
  else
wenzelm@28500
    88
    "$ISABELLE_TOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")"
berghofe@11813
    89
  fi
wenzelm@11843
    90
  RC="$?"
wenzelm@11801
    91
wenzelm@11801
    92
  if [ -n "$PDF" ]; then
wenzelm@11843
    93
    "$ISABELLE_EPSTOPDF" "$OUTFILE" || fail "Failed to produce pdf output"
wenzelm@11801
    94
  fi
wenzelm@11801
    95
wenzelm@20569
    96
  rm -f "$PRIVATE_FILE"
wenzelm@9794
    97
fi
wenzelm@11843
    98
wenzelm@11843
    99
exit "$RC"