src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

         SOME "smart" => NONE
       | _ => SOME (lookup_int name)
     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 =
       if auto then
         Smart_Type_Sys true