diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java index 8edea689cd6..6313e78e7df 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java @@ -131,52 +131,56 @@ public void taskFinished(TaskFinishedInfo info) { super.taskFinished(info); progressMax = 0; // reset progress bar marker final Proof proof = info.getProof(); + final Object result = info.getResult(); if (proof == null) { - final Object error = info.getResult(); LOGGER.info("Proof loading failed"); - if (error instanceof Throwable) { - LOGGER.info("Proof loading failed", (Throwable) error); + if (result instanceof Throwable thrown) { + LOGGER.info("Proof loading failed", thrown); } else { LOGGER.info("Proof loading failed"); } System.exit(1); } final int openGoals = proof.openGoals().size(); - final Object result2 = info.getResult(); if (info.getSource() instanceof ProverCore || info.getSource() instanceof ProofMacro) { if (!isAtLeastOneMacroRunning()) { - printResults(openGoals, info, result2); + printResults(openGoals, info, result); } } else if (info.getSource() instanceof ProblemLoader) { - LOGGER.debug("{}", result2); - System.exit(-1); - } - if (loadOnly || openGoals == 0) { - LOGGER.info("Number of open goals after loading: {}", openGoals); - System.exit(0); - } - ProblemLoader problemLoader = (ProblemLoader) info.getSource(); - if (problemLoader.hasProofScript()) { - try { - ProofScriptEntry script = problemLoader.getProofScript(); - if (script != null) { - ProofScriptEngine pse = - new ProofScriptEngine(script.script(), script.location()); - this.taskStarted( - new DefaultTaskStartedInfo(TaskKind.Macro, "Script started", 0)); - pse.execute(this, proof); - // The start and end messages are fake to persuade the system ... - // All this here should refactored anyway ... - this.taskFinished(new ProofMacroFinishedInfo(new SkipMacro(), proof)); + if (result != null) { + LOGGER.debug("{}", result); + if (result instanceof Throwable thrown) { + LOGGER.debug("Exception: ", thrown); } - } catch (Exception e) { - LOGGER.debug("", e); System.exit(-1); } - } else if (macroChosen()) { - applyMacro(); - } else { - finish(proof); + if (loadOnly || openGoals == 0) { + LOGGER.info("Number of open goals after loading: {}", openGoals); + System.exit(0); + } + ProblemLoader problemLoader = (ProblemLoader) info.getSource(); + if (problemLoader.hasProofScript()) { + try { + ProofScriptEntry script = problemLoader.getProofScript(); + if (script != null) { + ProofScriptEngine pse = + new ProofScriptEngine(script.script(), script.location()); + this.taskStarted( + new DefaultTaskStartedInfo(TaskKind.Macro, "Script started", 0)); + pse.execute(this, proof); + // The start and end messages are fake to persuade the system ... + // All this here should refactored anyway ... + this.taskFinished(new ProofMacroFinishedInfo(new SkipMacro(), proof)); + } + } catch (Exception e) { + LOGGER.debug("", e); + System.exit(-1); + } + } else if (macroChosen()) { + applyMacro(); + } else { + finish(proof); + } } }