1. changed configuration variables for linear programming (Cplex_tools):
LP_SOLVER is either CPLEX or GLPK
CPLEX_PATH is the path to the cplex binary
GLPK_PATH is the path to the glpk binary
The change makes it possible to switch between glpk and cplex at runtime.
2. moved conflicting list theories out of Library.thy into ROOT.ML
#!/usr/bin/env bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: get values from Isabelle settings environment
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: $PRG [OPTIONS] [VARNAMES ...]"
echo
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
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