If one by mistake press the "start theorem prover" twice one gets an error like: "Only a single prover can be running at any time - stop the running prover before launching a new one". The IDE should catch this kind of problem. The error message is ok but it should not come out as an error in the Error Log