option -o FILE --output to FILE (ps, eps, pdf);
authorwenzelm
Tue Oct 16 17:25:44 2001 +0200 (2001-10-16)
changeset 118019505bd5e9a36
parent 11800 5f84c687ba06
child 11802 1d5f5d2427d2
option -o FILE --output to FILE (ps, eps, pdf);
lib/Tools/browser
     1.1 --- a/lib/Tools/browser	Tue Oct 16 17:24:33 2001 +0200
     1.2 +++ b/lib/Tools/browser	Tue Oct 16 17:25:44 2001 +0200
     1.3 @@ -16,22 +16,34 @@
     1.4    echo
     1.5    echo "  Options are:"
     1.6    echo "    -d           delete file after use"
     1.7 +  echo "    -o FILE      output to FILE (ps, eps, pdf)"
     1.8    echo
     1.9    exit 1
    1.10  }
    1.11  
    1.12 +function fail()
    1.13 +{
    1.14 +  echo "$1" >&2
    1.15 +  exit 2
    1.16 +}
    1.17 +
    1.18 +
    1.19  ## process command line
    1.20  
    1.21  # options
    1.22  
    1.23  DELETE=""
    1.24 +OUTFILE=""
    1.25  
    1.26 -while getopts "d" OPT
    1.27 +while getopts "do:" OPT
    1.28  do
    1.29    case "$OPT" in
    1.30      d)
    1.31        DELETE=true
    1.32        ;;
    1.33 +    o)
    1.34 +      OUTFILE="$OPTARG"
    1.35 +      ;;
    1.36      \?)
    1.37        usage
    1.38        ;;
    1.39 @@ -55,7 +67,23 @@
    1.40    cd "$ISABELLE_BROWSER_INFO"
    1.41    exec java GraphBrowser.GraphBrowser
    1.42  else
    1.43 -  java GraphBrowser.GraphBrowser "$GRAPHFILE"
    1.44 +  case "$OUTFILE" in
    1.45 +    *.pdf)
    1.46 +      TMPOUTFILE="${OUTFILE%.pdf}.eps"
    1.47 +      PDF=true
    1.48 +      ;;
    1.49 +    *)
    1.50 +      TMPOUTFILE="$OUTFILE"
    1.51 +      PDF=""
    1.52 +      ;;
    1.53 +  esac
    1.54 +
    1.55 +  java GraphBrowser.GraphBrowser "$GRAPHFILE" "$TMPOUTFILE"
    1.56 +
    1.57 +  if [ -n "$PDF" ]; then
    1.58 +    "$ISABELLE_EPSTOPDF" "$TMPOUTFILE" || fail "Failed to produce pdf output"
    1.59 +    rm -f "$TMPOUTFILE"
    1.60 +  fi
    1.61 +
    1.62    [ -n "$DELETE" ] && rm -f "$GRAPHFILE"
    1.63  fi
    1.64 -