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