lib/Tools/getenv
author wenzelm
Wed Sep 30 21:32:44 2015 +0200 (2015-09-30)
changeset 61294 2d3d26e9b191
parent 47674 cdf95042e09c
child 62828 3fee575c9dce
permissions -rwxr-xr-x
renamed jvmpath to platform_path;
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@2296
     2
#
wenzelm@9788
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm@2307
     4
#
wenzelm@2734
     5
# DESCRIPTION: get values from Isabelle settings environment
wenzelm@2307
     6
wenzelm@2296
     7
wenzelm@2733
     8
## diagnostics
wenzelm@2733
     9
wenzelm@10511
    10
PRG="$(basename "$0")"
wenzelm@2296
    11
wenzelm@2296
    12
function usage()
wenzelm@2296
    13
{
wenzelm@2296
    14
  echo
wenzelm@28650
    15
  echo "Usage: isabelle $PRG [OPTIONS] [VARNAMES ...]"
wenzelm@2296
    16
  echo
wenzelm@2733
    17
  echo "  Options are:"
wenzelm@2733
    18
  echo "    -a           display complete environment"
wenzelm@2733
    19
  echo "    -b           print values only (doesn't work for -a)"
wenzelm@31497
    20
  echo "    -d FILE      dump complete environment to FILE"
wenzelm@31497
    21
  echo "                 (null terminated entries)"
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@31497
    35
DUMP=""
wenzelm@2733
    36
wenzelm@31497
    37
while getopts "abd:" OPT
wenzelm@2733
    38
do
wenzelm@2733
    39
  case "$OPT" in
wenzelm@2733
    40
    a)
wenzelm@2733
    41
      ALL=true
wenzelm@2733
    42
      ;;
wenzelm@2733
    43
    b)
wenzelm@2733
    44
      BASE=true
wenzelm@2733
    45
      ;;
wenzelm@31497
    46
    d)
wenzelm@31497
    47
      DUMP="$OPTARG"
wenzelm@31497
    48
      ;;
wenzelm@2733
    49
    \?)
wenzelm@2733
    50
      usage
wenzelm@2733
    51
      ;;
wenzelm@2733
    52
  esac
wenzelm@2733
    53
done
wenzelm@2733
    54
wenzelm@2733
    55
shift $(($OPTIND - 1))
wenzelm@2733
    56
wenzelm@2733
    57
wenzelm@2733
    58
# args
wenzelm@2733
    59
wenzelm@9788
    60
[ -n "$ALL" -a "$#" -ne 0 ] && usage
wenzelm@2733
    61
wenzelm@2733
    62
wenzelm@2296
    63
## main
wenzelm@2296
    64
wenzelm@2733
    65
if [ -n "$ALL" ]; then
wenzelm@17226
    66
  env
wenzelm@2733
    67
else
wenzelm@9788
    68
  for VAR in "$@"
wenzelm@2733
    69
  do
wenzelm@2733
    70
    if [ -n "$BASE" ]; then
wenzelm@2733
    71
      eval "echo \$$VAR"
wenzelm@2733
    72
    else
wenzelm@2733
    73
      eval "echo $VAR=\$$VAR"
wenzelm@2733
    74
    fi
wenzelm@2733
    75
  done
wenzelm@2733
    76
fi
wenzelm@31497
    77
wenzelm@31497
    78
if [ -n "$DUMP" ]; then
wenzelm@61294
    79
  export PATH_JVM="$(platform_path "$PATH")"
wenzelm@31497
    80
  exec perl -w -e 'for $key (keys %ENV) { print $key, "=", $ENV{$key}, "\x00"; }' > "$DUMP"
wenzelm@31497
    81
fi
wenzelm@31497
    82