lib/Tools/browser
author wenzelm
Wed, 31 Mar 2021 11:24:46 +0200
changeset 73772 d3f2038198ae
parent 62589 b5783412bfed
permissions -rwxr-xr-x
clarified (again): local tip could be actually more recent;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10511
diff changeset
     1
#!/usr/bin/env bash
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
     2
#
9788
wenzelm
parents: 9237
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
     4
#
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
     5
# DESCRIPTION: Isabelle graph browser
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
     6
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
     7
10511
wenzelm
parents: 9794
diff changeset
     8
PRG="$(basename "$0")"
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
     9
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    10
function usage()
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    11
{
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    12
  echo
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 28500
diff changeset
    13
  echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]"
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    14
  echo
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    15
  echo "  Options are:"
35587
f037aa6699c3 isabelle browser -b: Admin/build only;
wenzelm
parents: 34297
diff changeset
    16
  echo "    -b           Admin/build only"
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    17
  echo "    -c           cleanup -- remove GRAPHFILE after use"
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    18
  echo "    -o FILE      output to FILE (ps, eps, pdf)"
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    19
  echo
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    20
  exit 1
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    21
}
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    22
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    23
function fail()
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    24
{
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    25
  echo "$1" >&2
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    26
  exit 2
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    27
}
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    28
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    29
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    30
## process command line
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    31
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    32
# options
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    33
35587
f037aa6699c3 isabelle browser -b: Admin/build only;
wenzelm
parents: 34297
diff changeset
    34
ADMIN_BUILD=""
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    35
CLEAN=""
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    36
OUTFILE=""
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    37
35587
f037aa6699c3 isabelle browser -b: Admin/build only;
wenzelm
parents: 34297
diff changeset
    38
while getopts "bco:" OPT
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    39
do
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    40
  case "$OPT" in
35587
f037aa6699c3 isabelle browser -b: Admin/build only;
wenzelm
parents: 34297
diff changeset
    41
    b)
f037aa6699c3 isabelle browser -b: Admin/build only;
wenzelm
parents: 34297
diff changeset
    42
      ADMIN_BUILD=true
f037aa6699c3 isabelle browser -b: Admin/build only;
wenzelm
parents: 34297
diff changeset
    43
      ;;
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    44
    c)
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    45
      CLEAN=true
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    46
      ;;
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    47
    o)
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    48
      OUTFILE="$OPTARG"
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    49
      ;;
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    50
    \?)
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    51
      usage
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    52
      ;;
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    53
  esac
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    54
done
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    55
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    56
shift $(($OPTIND - 1))
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    57
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    58
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    59
# args
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    60
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    61
GRAPHFILE=""
9788
wenzelm
parents: 9237
diff changeset
    62
[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
wenzelm
parents: 9237
diff changeset
    63
[ "$#" -ne 0 ] && usage
7766
444ac56ead91 New option -d for deleting file after use.
berghofe
parents: 3640
diff changeset
    64
3640
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    65
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    66
## main
7554be69fd09 Startup script for Isabelle theory browser.
berghofe
parents:
diff changeset
    67
52443
725916b7dee5 more formal isabelle_admin_build;
wenzelm
parents: 49562
diff changeset
    68
isabelle_admin_build browser || exit $?
34283
7911e83d06c0 simplified build/bootstrap of graph browser -- avoid make;
wenzelm
parents: 29143
diff changeset
    69
27907
5b9bc956cec6 refined JVM path wrappers;
wenzelm
parents: 26230
diff changeset
    70
classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
25650
ce061f5083d7 added javapath (for cygwin);
wenzelm
parents: 20569
diff changeset
    71
35587
f037aa6699c3 isabelle browser -b: Admin/build only;
wenzelm
parents: 34297
diff changeset
    72
if [ -n "$GRAPHFILE" ]; then
58639
1df53737c59b prefer Unix standard-conformant $TMPDIR over hard-wired /tmp;
wenzelm
parents: 57082
diff changeset
    73
  PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE")
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    74
  if [ -n "$CLEAN" ]; then
49562
ba9dcdbf45f1 proper error message;
wenzelm
parents: 35587
diff changeset
    75
    mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE"
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    76
  else
49562
ba9dcdbf45f1 proper error message;
wenzelm
parents: 35587
diff changeset
    77
    cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE"
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    78
  fi
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
    79
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    80
  PDF=""
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    81
  case "$OUTFILE" in
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    82
    *.pdf)
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    83
      OUTFILE="${OUTFILE%%.pdf}.eps"
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    84
      PDF=true
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    85
      ;;
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    86
  esac
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    87
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    88
  if [ -z "$OUTFILE" ]; then
62589
b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents: 61294
diff changeset
    89
    isabelle java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
11813
berghofe
parents: 11801
diff changeset
    90
  else
62589
b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents: 61294
diff changeset
    91
    isabelle java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
11813
berghofe
parents: 11801
diff changeset
    92
  fi
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
    93
  RC="$?"
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    94
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
    95
  if [ -n "$PDF" ]; then
57082
2c1c8b38e3f0 more portable -- accomodate MiKTeX on Windows;
wenzelm
parents: 52443
diff changeset
    96
    (
2c1c8b38e3f0 more portable -- accomodate MiKTeX on Windows;
wenzelm
parents: 52443
diff changeset
    97
      cd "$(dirname "$OUTFILE")"
2c1c8b38e3f0 more portable -- accomodate MiKTeX on Windows;
wenzelm
parents: 52443
diff changeset
    98
      "$ISABELLE_EPSTOPDF" "$(basename "$OUTFILE")" || fail "Failed to produce pdf output"
2c1c8b38e3f0 more portable -- accomodate MiKTeX on Windows;
wenzelm
parents: 52443
diff changeset
    99
    )
11801
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
   100
  fi
9505bd5e9a36 option -o FILE --output to FILE (ps, eps, pdf);
wenzelm
parents: 10555
diff changeset
   101
20569
c315ba088073 renamed option -d to -c (cf. isatool display);
wenzelm
parents: 14981
diff changeset
   102
  rm -f "$PRIVATE_FILE"
35587
f037aa6699c3 isabelle browser -b: Admin/build only;
wenzelm
parents: 34297
diff changeset
   103
elif [ -z "$ADMIN_BUILD" ]; then
f037aa6699c3 isabelle browser -b: Admin/build only;
wenzelm
parents: 34297
diff changeset
   104
  [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
62589
b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents: 61294
diff changeset
   105
  exec isabelle java GraphBrowser.GraphBrowser
35587
f037aa6699c3 isabelle browser -b: Admin/build only;
wenzelm
parents: 34297
diff changeset
   106
else
f037aa6699c3 isabelle browser -b: Admin/build only;
wenzelm
parents: 34297
diff changeset
   107
  RC=0
9794
2be239143d42 fixed quoting;
wenzelm
parents: 9788
diff changeset
   108
fi
11843
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
   109
3dc60e93064f -o pdf: produce *both* eps and pdf;
wenzelm
parents: 11813
diff changeset
   110
exit "$RC"