lib/Tools/getenv
author wenzelm
Thu Nov 30 20:10:29 2000 +0100 (2000-11-30)
changeset 10555 2323ec838401
parent 10511 efb3428c9879
child 14981 e73f8140af78
permissions -rwxr-xr-x
/usr/bin/env bash;
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@2296
     2
#
wenzelm@2307
     3
# $Id$
wenzelm@9788
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@9788
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@2307
     6
#
wenzelm@2734
     7
# DESCRIPTION: get values from Isabelle settings environment
wenzelm@2307
     8
wenzelm@2296
     9
wenzelm@2733
    10
## diagnostics
wenzelm@2733
    11
wenzelm@10511
    12
PRG="$(basename "$0")"
wenzelm@2296
    13
wenzelm@2296
    14
function usage()
wenzelm@2296
    15
{
wenzelm@2296
    16
  echo
wenzelm@2733
    17
  echo "Usage: $PRG [OPTIONS] [VARNAMES ...]"
wenzelm@2296
    18
  echo
wenzelm@2733
    19
  echo "  Options are:"
wenzelm@2733
    20
  echo "    -a           display complete environment"
wenzelm@2733
    21
  echo "    -b           print values only (doesn't work for -a)"
wenzelm@2733
    22
  echo
wenzelm@2733
    23
  echo "  Get value of VARNAMES from the Isabelle settings."
wenzelm@2296
    24
  echo
wenzelm@2296
    25
  exit 1
wenzelm@2296
    26
}
wenzelm@2296
    27
wenzelm@2296
    28
wenzelm@2733
    29
## process command line
wenzelm@2733
    30
wenzelm@2733
    31
# options
wenzelm@2733
    32
wenzelm@2733
    33
ALL=""
wenzelm@2733
    34
BASE=""
wenzelm@2733
    35
wenzelm@2733
    36
while getopts "ab" OPT
wenzelm@2733
    37
do
wenzelm@2733
    38
  case "$OPT" in
wenzelm@2733
    39
    a)
wenzelm@2733
    40
      ALL=true
wenzelm@2733
    41
      ;;
wenzelm@2733
    42
    b)
wenzelm@2733
    43
      BASE=true
wenzelm@2733
    44
      ;;
wenzelm@2733
    45
    \?)
wenzelm@2733
    46
      usage
wenzelm@2733
    47
      ;;
wenzelm@2733
    48
  esac
wenzelm@2733
    49
done
wenzelm@2733
    50
wenzelm@2733
    51
shift $(($OPTIND - 1))
wenzelm@2733
    52
wenzelm@2733
    53
wenzelm@2733
    54
# args
wenzelm@2733
    55
wenzelm@9788
    56
[ -n "$ALL" -a "$#" -ne 0 ] && usage
wenzelm@2733
    57
wenzelm@2733
    58
wenzelm@2296
    59
## main
wenzelm@2296
    60
wenzelm@2733
    61
if [ -n "$ALL" ]; then
wenzelm@2733
    62
  env | sort
wenzelm@2733
    63
else
wenzelm@9788
    64
  for VAR in "$@"
wenzelm@2733
    65
  do
wenzelm@2733
    66
    if [ -n "$BASE" ]; then
wenzelm@2733
    67
      eval "echo \$$VAR"
wenzelm@2733
    68
    else
wenzelm@2733
    69
      eval "echo $VAR=\$$VAR"
wenzelm@2733
    70
    fi
wenzelm@2733
    71
  done
wenzelm@2733
    72
fi