# HG changeset patch
# User blanchet
# Date 1443814311 -7200
# Node ID b089c00f4db0c8cca2c400dff4ce2162fc162107
# Parent  ea605d019e9f361eb3d00375f0d041a2d1659b02
updated docs and NEWS

diff -r ea605d019e9f -r b089c00f4db0 NEWS
--- a/NEWS	Fri Oct 02 21:29:09 2015 +0200
+++ b/NEWS	Fri Oct 02 21:31:51 2015 +0200
@@ -249,9 +249,11 @@
   - Handle Vampire 4.0 proof output without raising exception.
   - Eliminated "MASH" environment variable. Use the "MaSh" option in
     Isabelle/jEdit instead. INCOMPATIBILITY.
+  - Eliminated obsolete "blocking" option and related subcommands.
 
 * Nitpick:
   - Removed "check_potential" and "check_genuine" options.
+  - Eliminated obsolete "blocking" option.
 
 * New commands lift_bnf and copy_bnf for lifting (copying) a BNF structure
   on the raw type to an abstract type defined using typedef.
diff -r ea605d019e9f -r b089c00f4db0 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Oct 02 21:29:09 2015 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Oct 02 21:31:51 2015 +0200
@@ -345,9 +345,7 @@
 \textit{compress} (\S\ref{output-format}).
 
 \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
-provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
-asynchronously you should not hesitate to raise this limit to 60 or 120 seconds
-if you are the kind of user who can think clearly while ATPs are active.
+provers' time limit. It is set to 30 seconds by default.
 \end{enum}
 
 Options can be set globally using \textbf{sledgehammer\_params}
@@ -579,11 +577,6 @@
 \item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on
 subgoal number \qty{num} (1 by default), with the given options and facts.
 
-\item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued
-by Sledgehammer. This allows you to examine results that might have been lost
-due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a
-limit on the number of messages to display (10 by default).
-
 \item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of
 automatic provers supported by Sledgehammer. See \S\ref{installation} and
 \S\ref{mode-of-operation} for more information on how to install automatic
@@ -729,8 +722,8 @@
 \end{enum}
 
 Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
-have a negative counterpart (e.g., \textit{blocking} vs.\
-\textit{non\_blocking}). When setting Boolean options or their negative
+have a negative counterpart (e.g., \textit{minimize} vs.\
+\textit{dont\_minimize}). When setting Boolean options or their negative
 counterparts, ``= \textit{true\/}'' may be omitted.
 
 \subsection{Mode of Operation}
@@ -920,14 +913,6 @@
 \opnodefault{prover}{string}
 Alias for \textit{provers}.
 
-\opfalse{blocking}{non\_blocking}
-Specifies whether the \textbf{sledgehammer} command should operate
-synchronously. The asynchronous (non-blocking) mode lets the user start proving
-the putative theorem manually while Sledgehammer looks for a proof, but it can
-also be more confusing. Irrespective of the value of this option, Sledgehammer
-is always run synchronously if \textit{debug} (\S\ref{output-format}) is
-enabled.
-
 \optrue{slice}{dont\_slice}
 Specifies whether the time allocated to a prover should be sliced into several
 segments, each of which has its own set of possibly prover-dependent options.
@@ -1235,8 +1220,7 @@
 \opfalse{debug}{no\_debug}
 Specifies whether Sledgehammer should display additional debugging information
 beyond what \textit{verbose} already displays. Enabling \textit{debug} also
-enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation})
-behind the scenes.
+enables \textit{verbose} behind the scenes.
 
 \nopagebreak
 {\small See also \textit{spy} (\S\ref{mode-of-operation}) and
@@ -1287,13 +1271,11 @@
 problem.
 \end{enum}
 
-Sledgehammer emits an error (if \textit{blocking} is enabled) or a warning
-(otherwise) if the actual outcome differs from the expected outcome. This option
-is useful for regression testing.
+Sledgehammer emits an error if the actual outcome differs from the expected outcome. This option is
+useful for regression testing.
 
 \nopagebreak
-{\small See also \textit{blocking} (\S\ref{mode-of-operation}) and
-\textit{timeout} (\S\ref{timeouts}).}
+{\small See also \textit{timeout} (\S\ref{timeouts}).}
 \end{enum}
 
 \subsection{Timeouts}