lib/Tools/browser

adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc

#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: Isabelle graph browser


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

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]"
  echo
  echo "  Options are:"
  echo "    -b           Admin/build only"
  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

ADMIN_BUILD=""
CLEAN=""
OUTFILE=""

while getopts "bco:" OPT
do
  case "$OPT" in
    b)
      ADMIN_BUILD=true
      ;;
    c)
      CLEAN=true
      ;;
    o)
      OUTFILE="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

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


## main

[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" browser || exit $?; }

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

if [ -n "$GRAPHFILE" ]; then
  PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
  if [ -n "$CLEAN" ]; then
    mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE"
  else
    cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE"
  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"
elif [ -z "$ADMIN_BUILD" ]; then
  [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
  exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
else
  RC=0
fi

exit "$RC"