1.1 --- a/etc/settings	Tue Jul 19 17:21:45 2005 +0200
     1.2 +++ b/etc/settings	Tue Jul 19 17:21:46 2005 +0200
     1.3 @@ -2,7 +2,11 @@
     1.4  # $Id$
     1.5  #
     1.6  # Isabelle settings -- site defaults.
     1.7 -# Do *NOT* copy this file into your personal isabelle directory!!!
     1.8 +#
     1.9 +# Important notes:
    1.10 +#   * See the system manual for explanations on Isabelle settings
    1.11 +#   * DO NOT EDIT the repository copy of this file!
    1.12 +#   * DO NOT COPY this file into your personal isabelle directory!
    1.13  
    1.14  ###
    1.15  ### ML compiler settings (ESSENTIAL!)
    1.16 @@ -12,7 +16,6 @@
    1.17  # binaries.  Do not invent new ML system names unless you know what
    1.18  # you are doing.  Only one of the sections below should be activated.
    1.19  
    1.20 -
    1.21  # try finding the poly packages from the Isabelle site in the usual places
    1.22  POLYML_HOME=$(choosefrom \
    1.23    "$ISABELLE_HOME/contrib/polyml" \
    1.24 @@ -63,7 +66,7 @@
    1.25  ### Compilation options (cf. isatool usedir)
    1.26  ###
    1.27  
    1.28 -ISABELLE_USEDIR_OPTIONS="-v true -i true"
    1.29 +ISABELLE_USEDIR_OPTIONS="-v true"
    1.30  
    1.31  # Specifically for the HOL image
    1.32  HOL_USEDIR_OPTIONS=""
    1.33 @@ -120,7 +123,7 @@
    1.34  
    1.35  
    1.36  ###
    1.37 -### default logic (users may want to override this in their own settings file)
    1.38 +### default logic
    1.39  ###
    1.40  
    1.41  ISABELLE_LOGIC=HOL
    1.42 @@ -175,21 +178,10 @@
    1.43  PROOFGENERAL_OPTIONS=""
    1.44  #PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true"
    1.45  
    1.46 -# try xemacs first, else emacs
    1.47 -type -path xemacs >/dev/null || PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS"
    1.48 +type -path xemacs >/dev/null || \
    1.49 +  PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS"
    1.50  
    1.51 -
    1.52 -# X-Symbol installation location (for Proof General, obsolete for PG >= 3.5)
    1.53 -XSYMBOL_HOME=$(choosefrom \
    1.54 -  "$ISABELLE_HOME/contrib/x-symbol" \
    1.55 -  "$ISABELLE_HOME/../x-symbol" \
    1.56 -  "/usr/share/x-symbol" \
    1.57 -  "/usr/local/x-symbol" \
    1.58 -  "/opt/x-symbol" \
    1.59 -  "")
    1.60 -
    1.61 -# Executed before xemacs with ProofGeneral is called.
    1.62 -# Required for remote fonts only.
    1.63 +# Executed before xemacs with ProofGeneral is called; required for remote fonts.
    1.64  #XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
    1.65  
    1.66  
    1.67 @@ -228,12 +220,8 @@
    1.68  
    1.69  # For configuring HOL/Matrix/cplex
    1.70  # First option: use the commercial cplex solver
    1.71 -# LP_SOLVER_NAME=CPLEX
    1.72 -# LP_SOLVER_PATH=cplex
    1.73 +#LP_SOLVER_NAME=CPLEX
    1.74 +#LP_SOLVER_PATH=cplex
    1.75  # Second option: use the open source glpk solver
    1.76 -# LP_SOLVER_NAME=GLPK
    1.77 -# LP_SOLVER_PATH=glpsol
    1.78 -
    1.79 -# toogles the detail of the error message in case of a cyclic definition
    1.80 -DEFS_CHAIN_HISTORY=ON
    1.81 -#DEFS_CHAIN_HISTORY=OFF
    1.82 \ No newline at end of file
    1.83 +#LP_SOLVER_NAME=GLPK
    1.84 +#LP_SOLVER_PATH=glpsol