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