lib/Tools/getenv
changeset 2733 1d1013313201
parent 2335 e965156e84e3
child 2734 e9bbef1b2fbe
equal deleted inserted replaced
2732:84fc9c3b6bf0 2733:1d1013313201
     3 # $Id$
     3 # $Id$
     4 #
     4 #
     5 # DESCRIPTION: get value from Isabelle settings
     5 # DESCRIPTION: get value from Isabelle settings
     6 
     6 
     7 
     7 
       
     8 ## diagnostics
       
     9 
     8 PRG=$(basename $0)
    10 PRG=$(basename $0)
     9 
    11 
    10 function usage()
    12 function usage()
    11 {
    13 {
    12   echo
    14   echo
    13   echo "Usage: $PRG VARNAME"
    15   echo "Usage: $PRG [OPTIONS] [VARNAMES ...]"
    14   echo
    16   echo
    15   echo "  Get value of VARNAME from the Isabelle settings."
    17   echo "  Options are:"
       
    18   echo "    -a           display complete environment"
       
    19   echo "    -b           print values only (doesn't work for -a)"
       
    20   echo
       
    21   echo "  Get value of VARNAMES from the Isabelle settings."
    16   echo
    22   echo
    17   exit 1
    23   exit 1
    18 }
    24 }
    19 
    25 
    20 
    26 
       
    27 ## process command line
       
    28 
       
    29 # options
       
    30 
       
    31 ALL=""
       
    32 BASE=""
       
    33 
       
    34 while getopts "ab" OPT
       
    35 do
       
    36   case "$OPT" in
       
    37     a)
       
    38       ALL=true
       
    39       ;;
       
    40     b)
       
    41       BASE=true
       
    42       ;;
       
    43     \?)
       
    44       usage
       
    45       ;;
       
    46   esac
       
    47 done
       
    48 
       
    49 shift $(($OPTIND - 1))
       
    50 
       
    51 
       
    52 # args
       
    53 
       
    54 [ -n "$ALL" -a $# -ne 0 ] && usage
       
    55 
       
    56 
    21 ## main
    57 ## main
    22 
    58 
    23 [ $# -ne 1 ] && usage
    59 if [ -n "$ALL" ]; then
    24 
    60   env | sort
    25 eval "echo \$$1"
    61 else
       
    62   for VAR in $*
       
    63   do
       
    64     if [ -n "$BASE" ]; then
       
    65       eval "echo \$$VAR"
       
    66     else
       
    67       eval "echo $VAR=\$$VAR"
       
    68     fi
       
    69   done
       
    70 fi