# HG changeset patch
# User blanchet
# Date 1440773285 -7200
# Node ID 0810068379d840a1c4942ff9a2b926c1f895552d
# Parent  c2155072c2f48b9cd6410e19514a33b234d9551a
eliminated obsolete environment variable

diff -r c2155072c2f4 -r 0810068379d8 NEWS
--- a/NEWS	Fri Aug 28 13:37:06 2015 +0200
+++ b/NEWS	Fri Aug 28 16:48:05 2015 +0200
@@ -193,6 +193,8 @@
     cases where Sledgehammer gives a proof that does not work.
   - Auto Sledgehammer now minimizes and preplays the results.
   - Handle Vampire 4.0 proof output without raising exception.
+  - Eliminated "MASH" environment variable. Use the "MaSh" option in
+    Isabelle/jEdit instead. INCOMPATIBILITY.
 
 * Nitpick:
   - Removed "check_potential" and "check_genuine" options.
diff -r c2155072c2f4 -r 0810068379d8 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Aug 28 13:37:06 2015 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Aug 28 16:48:05 2015 +0200
@@ -370,7 +370,7 @@
 
 Sledgehammer heuristically selects a few hundred relevant lemmas from the
 currently loaded libraries. The component that performs this selection is
-called \emph{relevance filter}.
+called \emph{relevance filter} (\S\ref{relevance-filter}).
 
 \begin{enum}
 \item[\labelitemi]
@@ -390,13 +390,10 @@
 \underline{S}ledge\underline{h}ammer). It applies machine learning to the
 problem of finding relevant facts.
 
-\item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh.
+\item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh. This is
+the default.
 \end{enum}
 
-The default is either MePo or MeSh, depending on whether the environment
-variable \texttt{MASH} is set and what class of provers the target prover
-belongs to (\S\ref{relevance-filter}).
-
 The number of facts included in a problem varies from prover to prover, since
 some provers get overwhelmed more easily than others. You can show the number of
 facts given using the \textit{verbose} option (\S\ref{output-format}) and the
@@ -1018,10 +1015,7 @@
 default (cf.\ \textit{smart} below).
 
 The default algorithm is \textit{nb\_knn}. The algorithm can be selected by
-setting \texttt{MASH}---either in the environment in which Isabelle is launched,
-in your
-\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak settings}
-file, or via the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle >
+setting the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle >
 General'' in Isabelle/jEdit. Persistent data for both algorithms is stored in
 the directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak
 mash}.
diff -r c2155072c2f4 -r 0810068379d8 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 28 13:37:06 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 28 16:48:05 2015 +0200
@@ -138,20 +138,18 @@
 | MaSh_NB_Ext
 | MaSh_kNN_Ext
 
-(* TODO: eliminate "MASH" environment variable after Isabelle2014 release *)
 fun mash_algorithm () =
-  let val flag1 = Options.default_string @{system_option MaSh} in
-    (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
-      "yes" => SOME MaSh_NB_kNN
-    | "sml" => SOME MaSh_NB_kNN
-    | "nb" => SOME MaSh_NB
-    | "knn" => SOME MaSh_kNN
-    | "nb_knn" => SOME MaSh_NB_kNN
-    | "nb_ext" => SOME MaSh_NB_Ext
-    | "knn_ext" => SOME MaSh_kNN_Ext
-    | "" => NONE
-    | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm ^ "."); NONE))
-  end
+  (case Options.default_string @{system_option MaSh} of
+    "yes" => SOME MaSh_NB_kNN
+  | "sml" => SOME MaSh_NB_kNN
+  | "nb" => SOME MaSh_NB
+  | "knn" => SOME MaSh_kNN
+  | "nb_knn" => SOME MaSh_NB_kNN
+  | "nb_ext" => SOME MaSh_NB_Ext
+  | "knn_ext" => SOME MaSh_kNN_Ext
+  | "none" => NONE
+  | "" => NONE
+  | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm ^ "."); NONE))
 
 val is_mash_enabled = is_some o mash_algorithm
 val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm