--- a/src/Pure/Tools/sledgehammer_params.scala Thu Nov 14 17:39:32 2013 +0100
+++ b/src/Pure/Tools/sledgehammer_params.scala Fri Nov 15 19:31:10 2013 +0100
@@ -37,13 +37,10 @@
def get_provers: String = synchronized { _provers }
private def sledgehammer_provers(
- prover: Session.Prover, output: Isabelle_Process.Output): Boolean =
+ prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
{
- output.body match {
- case Nil => update_provers(""); true
- case List(XML.Text(s)) => update_provers(s); true
- case _ => false
- }
+ update_provers(msg.text)
+ true
}
val functions =