lib/Tools/getenv
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 62828 3fee575c9dce
permissions -rwxr-xr-x
more robust sorted_entries;
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@62828
    60
[ -z "$ALL" -a -z "$DUMP" -a "$#" -eq 0 ] && usage
wenzelm@9788
    61
[ -n "$ALL" -a "$#" -ne 0 ] && usage
wenzelm@2733
    62
wenzelm@2733
    63
wenzelm@2296
    64
## main
wenzelm@2296
    65
wenzelm@2733
    66
if [ -n "$ALL" ]; then
wenzelm@17226
    67
  env
wenzelm@2733
    68
else
wenzelm@9788
    69
  for VAR in "$@"
wenzelm@2733
    70
  do
wenzelm@2733
    71
    if [ -n "$BASE" ]; then
wenzelm@2733
    72
      eval "echo \$$VAR"
wenzelm@2733
    73
    else
wenzelm@2733
    74
      eval "echo $VAR=\$$VAR"
wenzelm@2733
    75
    fi
wenzelm@2733
    76
  done
wenzelm@2733
    77
fi
wenzelm@31497
    78
wenzelm@31497
    79
if [ -n "$DUMP" ]; then
wenzelm@61294
    80
  export PATH_JVM="$(platform_path "$PATH")"
wenzelm@31497
    81
  exec perl -w -e 'for $key (keys %ENV) { print $key, "=", $ENV{$key}, "\x00"; }' > "$DUMP"
wenzelm@31497
    82
fi
wenzelm@31497
    83