lib/Tools/getenv
author wenzelm
Mon, 08 Nov 2021 13:51:24 +0100
changeset 74732 015282fb3e31
parent 74644 549019b4a808
permissions -rwxr-xr-x
clarified messages, depending on option "document_echo";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10511
diff changeset
     1
#!/usr/bin/env bash
2296
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
     2
#
9788
wenzelm
parents: 3007
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
2307
508d2a233dbc *** empty log message ***
wenzelm
parents: 2296
diff changeset
     4
#
2734
e9bbef1b2fbe improved DESCRIPTION;
wenzelm
parents: 2733
diff changeset
     5
# DESCRIPTION: get values from Isabelle settings environment
2307
508d2a233dbc *** empty log message ***
wenzelm
parents: 2296
diff changeset
     6
2296
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
     7
2733
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
     8
## diagnostics
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
     9
10511
wenzelm
parents: 9788
diff changeset
    10
PRG="$(basename "$0")"
2296
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
    11
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
    12
function usage()
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
    13
{
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
    14
  echo
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 17226
diff changeset
    15
  echo "Usage: isabelle $PRG [OPTIONS] [VARNAMES ...]"
2296
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 "  Options are:"
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    18
  echo "    -a           display complete environment"
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    19
  echo "    -b           print values only (doesn't work for -a)"
73581
cd84e58aed26 eliminated perl: prefer elementary GNU printenv;
wenzelm
parents: 62828
diff changeset
    20
  echo "    -d FILE      dump complete environment to file (NUL terminated entries)"
2733
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    21
  echo
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    22
  echo "  Get value of VARNAMES from the Isabelle settings."
2296
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
    23
  echo
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
    24
  exit 1
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
    25
}
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
    26
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
    27
2733
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    28
## process command line
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    29
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    30
# options
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    31
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    32
ALL=""
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    33
BASE=""
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 29143
diff changeset
    34
DUMP=""
2733
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    35
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 29143
diff changeset
    36
while getopts "abd:" OPT
2733
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
      ;;
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 29143
diff changeset
    45
    d)
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 29143
diff changeset
    46
      DUMP="$OPTARG"
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 29143
diff changeset
    47
      ;;
2733
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    48
    \?)
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    49
      usage
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    50
      ;;
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    51
  esac
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    52
done
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    53
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    54
shift $(($OPTIND - 1))
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    55
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    56
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    57
# args
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    58
62828
3fee575c9dce clarified usage;
wenzelm
parents: 61294
diff changeset
    59
[ -z "$ALL" -a -z "$DUMP" -a "$#" -eq 0 ] && usage
9788
wenzelm
parents: 3007
diff changeset
    60
[ -n "$ALL" -a "$#" -ne 0 ] && usage
2733
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    61
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    62
2296
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
    63
## main
3b1086cf2f4d getenv: get value from Isabelle settings.
wenzelm
parents:
diff changeset
    64
2733
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    65
if [ -n "$ALL" ]; then
17226
0687c76021c0 refrain from sorting output;
wenzelm
parents: 14981
diff changeset
    66
  env
2733
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    67
else
9788
wenzelm
parents: 3007
diff changeset
    68
  for VAR in "$@"
2733
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    69
  do
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    70
    if [ -n "$BASE" ]; then
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    71
      eval "echo \$$VAR"
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    72
    else
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    73
      eval "echo $VAR=\$$VAR"
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    74
    fi
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    75
  done
1d1013313201 added -a, -b options;
wenzelm
parents: 2335
diff changeset
    76
fi
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 29143
diff changeset
    77
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 29143
diff changeset
    78
if [ -n "$DUMP" ]; then
61294
2d3d26e9b191 renamed jvmpath to platform_path;
wenzelm
parents: 47674
diff changeset
    79
  export PATH_JVM="$(platform_path "$PATH")"
74644
549019b4a808 more robust;
wenzelm
parents: 73581
diff changeset
    80
  if [ -e "$ISABELLE_PRINTENV" ]; then
549019b4a808 more robust;
wenzelm
parents: 73581
diff changeset
    81
    "$ISABELLE_PRINTENV" -0 > "$DUMP"
549019b4a808 more robust;
wenzelm
parents: 73581
diff changeset
    82
  else
549019b4a808 more robust;
wenzelm
parents: 73581
diff changeset
    83
    exit 2
549019b4a808 more robust;
wenzelm
parents: 73581
diff changeset
    84
  fi
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 29143
diff changeset
    85
fi