# HG changeset patch
# User wenzelm
# Date 857578436 -3600
# Node ID 1d101331320105ba58cf1eb6cb0aa67d2df1df0f
# Parent  84fc9c3b6bf0faee7ae2130e56668ca79f6fcb4e
added -a, -b options;
multiple VARNAMES;

diff -r 84fc9c3b6bf0 -r 1d1013313201 lib/Tools/getenv
--- a/lib/Tools/getenv	Wed Mar 05 14:19:34 1997 +0100
+++ b/lib/Tools/getenv	Wed Mar 05 17:13:56 1997 +0100
@@ -5,21 +5,66 @@
 # DESCRIPTION: get value from Isabelle settings
 
 
+## diagnostics
+
 PRG=$(basename $0)
 
 function usage()
 {
   echo
-  echo "Usage: $PRG VARNAME"
+  echo "Usage: $PRG [OPTIONS] [VARNAMES ...]"
   echo
-  echo "  Get value of VARNAME from the Isabelle settings."
+  echo "  Options are:"
+  echo "    -a           display complete environment"
+  echo "    -b           print values only (doesn't work for -a)"
+  echo
+  echo "  Get value of VARNAMES from the Isabelle settings."
   echo
   exit 1
 }
 
 
+## process command line
+
+# options
+
+ALL=""
+BASE=""
+
+while getopts "ab" OPT
+do
+  case "$OPT" in
+    a)
+      ALL=true
+      ;;
+    b)
+      BASE=true
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ -n "$ALL" -a $# -ne 0 ] && usage
+
+
 ## main
 
-[ $# -ne 1 ] && usage
-
-eval "echo \$$1"
+if [ -n "$ALL" ]; then
+  env | sort
+else
+  for VAR in $*
+  do
+    if [ -n "$BASE" ]; then
+      eval "echo \$$VAR"
+    else
+      eval "echo $VAR=\$$VAR"
+    fi
+  done
+fi