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