| 10555 |      1 | #!/usr/bin/env bash
 | 
| 2296 |      2 | #
 | 
| 9788 |      3 | # Author: Markus Wenzel, TU Muenchen
 | 
| 2307 |      4 | #
 | 
| 2734 |      5 | # DESCRIPTION: get values from Isabelle settings environment
 | 
| 2307 |      6 | 
 | 
| 2296 |      7 | 
 | 
| 2733 |      8 | ## diagnostics
 | 
|  |      9 | 
 | 
| 10511 |     10 | PRG="$(basename "$0")"
 | 
| 2296 |     11 | 
 | 
|  |     12 | function usage()
 | 
|  |     13 | {
 | 
|  |     14 |   echo
 | 
| 28650 |     15 |   echo "Usage: isabelle $PRG [OPTIONS] [VARNAMES ...]"
 | 
| 2296 |     16 |   echo
 | 
| 2733 |     17 |   echo "  Options are:"
 | 
|  |     18 |   echo "    -a           display complete environment"
 | 
|  |     19 |   echo "    -b           print values only (doesn't work for -a)"
 | 
| 31497 |     20 |   echo "    -d FILE      dump complete environment to FILE"
 | 
|  |     21 |   echo "                 (null terminated entries)"
 | 
| 2733 |     22 |   echo
 | 
|  |     23 |   echo "  Get value of VARNAMES from the Isabelle settings."
 | 
| 2296 |     24 |   echo
 | 
|  |     25 |   exit 1
 | 
|  |     26 | }
 | 
|  |     27 | 
 | 
|  |     28 | 
 | 
| 2733 |     29 | ## process command line
 | 
|  |     30 | 
 | 
|  |     31 | # options
 | 
|  |     32 | 
 | 
|  |     33 | ALL=""
 | 
|  |     34 | BASE=""
 | 
| 31497 |     35 | DUMP=""
 | 
| 2733 |     36 | 
 | 
| 31497 |     37 | while getopts "abd:" OPT
 | 
| 2733 |     38 | do
 | 
|  |     39 |   case "$OPT" in
 | 
|  |     40 |     a)
 | 
|  |     41 |       ALL=true
 | 
|  |     42 |       ;;
 | 
|  |     43 |     b)
 | 
|  |     44 |       BASE=true
 | 
|  |     45 |       ;;
 | 
| 31497 |     46 |     d)
 | 
|  |     47 |       DUMP="$OPTARG"
 | 
|  |     48 |       ;;
 | 
| 2733 |     49 |     \?)
 | 
|  |     50 |       usage
 | 
|  |     51 |       ;;
 | 
|  |     52 |   esac
 | 
|  |     53 | done
 | 
|  |     54 | 
 | 
|  |     55 | shift $(($OPTIND - 1))
 | 
|  |     56 | 
 | 
|  |     57 | 
 | 
|  |     58 | # args
 | 
|  |     59 | 
 | 
| 62828 |     60 | [ -z "$ALL" -a -z "$DUMP" -a "$#" -eq 0 ] && usage
 | 
| 9788 |     61 | [ -n "$ALL" -a "$#" -ne 0 ] && usage
 | 
| 2733 |     62 | 
 | 
|  |     63 | 
 | 
| 2296 |     64 | ## main
 | 
|  |     65 | 
 | 
| 2733 |     66 | if [ -n "$ALL" ]; then
 | 
| 17226 |     67 |   env
 | 
| 2733 |     68 | else
 | 
| 9788 |     69 |   for VAR in "$@"
 | 
| 2733 |     70 |   do
 | 
|  |     71 |     if [ -n "$BASE" ]; then
 | 
|  |     72 |       eval "echo \$$VAR"
 | 
|  |     73 |     else
 | 
|  |     74 |       eval "echo $VAR=\$$VAR"
 | 
|  |     75 |     fi
 | 
|  |     76 |   done
 | 
|  |     77 | fi
 | 
| 31497 |     78 | 
 | 
|  |     79 | if [ -n "$DUMP" ]; then
 | 
| 61294 |     80 |   export PATH_JVM="$(platform_path "$PATH")"
 | 
| 31497 |     81 |   exec perl -w -e 'for $key (keys %ENV) { print $key, "=", $ENV{$key}, "\x00"; }' > "$DUMP"
 | 
|  |     82 | fi
 | 
|  |     83 | 
 |