# HG changeset patch
# User blanchet
# Date 1306485007 -7200
# Node ID e23f61546cf0850fb4e00c1b74a793937b6904e4
# Parent  fe291ab75eb577b56a6cfa0e05849e404008c7f0
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)

diff -r fe291ab75eb5 -r e23f61546cf0 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:07 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:07 2011 +0200
@@ -792,7 +792,9 @@
 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.
+also be more confusing. Irrespective of the value of this option, Sledgehammer
+is always run synchronously for the new jEdit-based user interface or if
+\textit{debug} (\S\ref{output-format}) is enabled.
 
 \optrue{slicing}{no\_slicing}
 Specifies whether the time allocated to a prover should be sliced into several
diff -r fe291ab75eb5 -r e23f61546cf0 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:07 2011 +0200
@@ -243,7 +243,9 @@
     val debug = not auto andalso lookup_bool "debug"
     val verbose = debug orelse (not auto andalso lookup_bool "verbose")
     val overlord = lookup_bool "overlord"
-    val blocking = auto orelse debug orelse lookup_bool "blocking"
+    val blocking =
+      Isabelle_Process.is_active () orelse auto orelse debug orelse
+      lookup_bool "blocking"
     val provers = lookup_string "provers" |> space_explode " "
                   |> auto ? single o hd
     val type_sys =