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