diff -r 22b5ecb53dd9 -r a578ebf5b78d src/Pure/PIDE/prover.scala --- a/src/Pure/PIDE/prover.scala Sun Apr 11 22:47:55 2021 +0200 +++ b/src/Pure/PIDE/prover.scala Mon Apr 12 11:45:16 2021 +0200 @@ -54,14 +54,14 @@ } } - class Protocol_Error(msg: String) extends Exception(msg) - def bad_header(print: String): Nothing = throw new Protocol_Error("bad message header: " + print) - def bad_chunks(): Nothing = throw new Protocol_Error("bad message chunks") + class Malformed(msg: String) extends Exn.User_Error("Malformed prover message: " + msg) + def bad_header(print: String): Nothing = throw new Malformed("bad message header\n" + print) + def bad_chunks(): Nothing = throw new Malformed("bad message chunks") def the_chunk(chunks: List[Bytes], print: => String): Bytes = chunks match { case List(chunk) => chunk - case _ => throw new Protocol_Error("single chunk expected: " + print) + case _ => throw new Malformed("single chunk expected: " + print) } class Protocol_Output(props: Properties.T, val chunks: List[Bytes]) @@ -289,7 +289,7 @@ } catch { case e: IOException => system_output("Cannot read message:\n" + e.getMessage) - case e: Prover.Protocol_Error => system_output("Malformed message:\n" + e.getMessage) + case e: Prover.Malformed => system_output(e.getMessage) } stream.close()