#!/usr/bin/env bash

#

# $Id$

# Author: Markus Wenzel, TU Muenchen

#

# DESCRIPTION: Isabelle graph browser

PRG="$(basename "$0")"

function usage()

{

  echo

  echo "Usage: $PRG [OPTIONS] [GRAPHFILE]"

  echo

  echo "  Options are:"

  echo "    -c           cleanup -- remove GRAPHFILE after use"

  echo "    -o FILE      output to FILE (ps, eps, pdf)"

  echo

  exit 1

}

function fail()

{

  echo "$1" >&2

  exit 2

}

## process command line

# options

CLEAN=""

OUTFILE=""

while getopts "co:" OPT

do

  case "$OPT" in

    c)

      CLEAN=true

      ;;

    o)

      OUTFILE="$OPTARG"

      ;;

    \?)

      usage

      ;;

  esac

done

shift $(($OPTIND - 1))

# args

GRAPHFILE=""

[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }

[ "$#" -ne 0 ] && usage

## main

classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"

if [ -z "$GRAPHFILE" ]; then

  [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"

  exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser

else

  PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")

  if [ -n "$CLEAN" ]; then

    mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"

  else

    cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $FILE"

  fi

  PDF=""

  case "$OUTFILE" in

    *.pdf)

      OUTFILE="${OUTFILE%%.pdf}.eps"

      PDF=true

      ;;

  esac

  if [ -z "$OUTFILE" ]; then

    "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")"

  else

    "$ISABELLE_TOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")"

  fi

  RC="$?"

  if [ -n "$PDF" ]; then

    "$ISABELLE_EPSTOPDF" "$OUTFILE" || fail "Failed to produce pdf output"

  fi

  rm -f "$PRIVATE_FILE"

fi

exit "$RC"