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