lib/Tools/browser
author wenzelm
Wed Nov 07 21:42:16 2018 +0100 (9 months ago)
changeset 69255 800b1ce96fce
parent 62589 b5783412bfed
permissions -rwxr-xr-x
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # DESCRIPTION: Isabelle graph browser
     6 
     7 
     8 PRG="$(basename "$0")"
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]"
    14   echo
    15   echo "  Options are:"
    16   echo "    -b           Admin/build only"
    17   echo "    -c           cleanup -- remove GRAPHFILE after use"
    18   echo "    -o FILE      output to FILE (ps, eps, pdf)"
    19   echo
    20   exit 1
    21 }
    22 
    23 function fail()
    24 {
    25   echo "$1" >&2
    26   exit 2
    27 }
    28 
    29 
    30 ## process command line
    31 
    32 # options
    33 
    34 ADMIN_BUILD=""
    35 CLEAN=""
    36 OUTFILE=""
    37 
    38 while getopts "bco:" OPT
    39 do
    40   case "$OPT" in
    41     b)
    42       ADMIN_BUILD=true
    43       ;;
    44     c)
    45       CLEAN=true
    46       ;;
    47     o)
    48       OUTFILE="$OPTARG"
    49       ;;
    50     \?)
    51       usage
    52       ;;
    53   esac
    54 done
    55 
    56 shift $(($OPTIND - 1))
    57 
    58 
    59 # args
    60 
    61 GRAPHFILE=""
    62 [ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
    63 [ "$#" -ne 0 ] && usage
    64 
    65 
    66 ## main
    67 
    68 isabelle_admin_build browser || exit $?
    69 
    70 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
    71 
    72 if [ -n "$GRAPHFILE" ]; then
    73   PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE")
    74   if [ -n "$CLEAN" ]; then
    75     mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE"
    76   else
    77     cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE"
    78   fi
    79 
    80   PDF=""
    81   case "$OUTFILE" in
    82     *.pdf)
    83       OUTFILE="${OUTFILE%%.pdf}.eps"
    84       PDF=true
    85       ;;
    86   esac
    87 
    88   if [ -z "$OUTFILE" ]; then
    89     isabelle java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
    90   else
    91     isabelle java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
    92   fi
    93   RC="$?"
    94 
    95   if [ -n "$PDF" ]; then
    96     (
    97       cd "$(dirname "$OUTFILE")"
    98       "$ISABELLE_EPSTOPDF" "$(basename "$OUTFILE")" || fail "Failed to produce pdf output"
    99     )
   100   fi
   101 
   102   rm -f "$PRIVATE_FILE"
   103 elif [ -z "$ADMIN_BUILD" ]; then
   104   [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
   105   exec isabelle java GraphBrowser.GraphBrowser
   106 else
   107   RC=0
   108 fi
   109 
   110 exit "$RC"