lib/Tools/browser
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 62589 b5783412bfed
permissions -rwxr-xr-x
more robust sorted_entries;
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@35587
    16
  echo "    -b           Admin/build only"
wenzelm@20569
    17
  echo "    -c           cleanup -- remove GRAPHFILE after use"
wenzelm@11801
    18
  echo "    -o FILE      output to FILE (ps, eps, pdf)"
berghofe@7766
    19
  echo
berghofe@3640
    20
  exit 1
berghofe@3640
    21
}
berghofe@3640
    22
wenzelm@11801
    23
function fail()
wenzelm@11801
    24
{
wenzelm@11801
    25
  echo "$1" >&2
wenzelm@11801
    26
  exit 2
wenzelm@11801
    27
}
wenzelm@11801
    28
wenzelm@11801
    29
berghofe@7766
    30
## process command line
berghofe@7766
    31
berghofe@7766
    32
# options
berghofe@7766
    33
wenzelm@35587
    34
ADMIN_BUILD=""
wenzelm@20569
    35
CLEAN=""
wenzelm@11801
    36
OUTFILE=""
berghofe@7766
    37
wenzelm@35587
    38
while getopts "bco:" OPT
berghofe@7766
    39
do
berghofe@7766
    40
  case "$OPT" in
wenzelm@35587
    41
    b)
wenzelm@35587
    42
      ADMIN_BUILD=true
wenzelm@35587
    43
      ;;
wenzelm@20569
    44
    c)
wenzelm@20569
    45
      CLEAN=true
berghofe@7766
    46
      ;;
wenzelm@11801
    47
    o)
wenzelm@11801
    48
      OUTFILE="$OPTARG"
wenzelm@11801
    49
      ;;
berghofe@7766
    50
    \?)
berghofe@7766
    51
      usage
berghofe@7766
    52
      ;;
berghofe@7766
    53
  esac
berghofe@7766
    54
done
berghofe@7766
    55
berghofe@7766
    56
shift $(($OPTIND - 1))
berghofe@7766
    57
berghofe@7766
    58
berghofe@7766
    59
# args
berghofe@7766
    60
berghofe@7766
    61
GRAPHFILE=""
wenzelm@9788
    62
[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
wenzelm@9788
    63
[ "$#" -ne 0 ] && usage
berghofe@7766
    64
berghofe@3640
    65
berghofe@3640
    66
## main
berghofe@3640
    67
wenzelm@52443
    68
isabelle_admin_build browser || exit $?
wenzelm@34283
    69
wenzelm@27907
    70
classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
wenzelm@25650
    71
wenzelm@35587
    72
if [ -n "$GRAPHFILE" ]; then
wenzelm@58639
    73
  PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE")
wenzelm@20569
    74
  if [ -n "$CLEAN" ]; then
wenzelm@49562
    75
    mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE"
wenzelm@20569
    76
  else
wenzelm@49562
    77
    cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE"
wenzelm@20569
    78
  fi
wenzelm@20569
    79
wenzelm@11843
    80
  PDF=""
wenzelm@11801
    81
  case "$OUTFILE" in
wenzelm@11801
    82
    *.pdf)
wenzelm@11843
    83
      OUTFILE="${OUTFILE%%.pdf}.eps"
wenzelm@11801
    84
      PDF=true
wenzelm@11801
    85
      ;;
wenzelm@11801
    86
  esac
wenzelm@11801
    87
wenzelm@11843
    88
  if [ -z "$OUTFILE" ]; then
wenzelm@62589
    89
    isabelle java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
berghofe@11813
    90
  else
wenzelm@62589
    91
    isabelle java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
berghofe@11813
    92
  fi
wenzelm@11843
    93
  RC="$?"
wenzelm@11801
    94
wenzelm@11801
    95
  if [ -n "$PDF" ]; then
wenzelm@57082
    96
    (
wenzelm@57082
    97
      cd "$(dirname "$OUTFILE")"
wenzelm@57082
    98
      "$ISABELLE_EPSTOPDF" "$(basename "$OUTFILE")" || fail "Failed to produce pdf output"
wenzelm@57082
    99
    )
wenzelm@11801
   100
  fi
wenzelm@11801
   101
wenzelm@20569
   102
  rm -f "$PRIVATE_FILE"
wenzelm@35587
   103
elif [ -z "$ADMIN_BUILD" ]; then
wenzelm@35587
   104
  [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
wenzelm@62589
   105
  exec isabelle java GraphBrowser.GraphBrowser
wenzelm@35587
   106
else
wenzelm@35587
   107
  RC=0
wenzelm@9794
   108
fi
wenzelm@11843
   109
wenzelm@11843
   110
exit "$RC"