--- a/src/Pure/PIDE/prover.scala Sun Apr 12 21:53:58 2020 +0100
+++ b/src/Pure/PIDE/prover.scala Mon Apr 13 16:16:22 2020 +0200
@@ -90,7 +90,7 @@
private def exit_message(result: Process_Result)
{
output(Markup.EXIT, Markup.Process_Result(result),
- List(XML.Text("Return code: " + result.rc.toString)))
+ List(XML.Text(result.print_return_code)))
}
--- a/src/Pure/System/process_result.scala Sun Apr 12 21:53:58 2020 +0100
+++ b/src/Pure/System/process_result.scala Mon Apr 13 16:16:22 2020 +0200
@@ -6,6 +6,12 @@
package isabelle
+object Process_Result
+{
+ def print_return_code(rc: Int): String = "Return code: " + rc
+ def print_rc(rc: Int): String = "return code " + rc
+}
+
final case class Process_Result(
rc: Int,
out_lines: List[String] = Nil,
@@ -36,6 +42,9 @@
def check: Process_Result = check_rc(_ == 0)
+ def print_return_code: String = Process_Result.print_return_code(rc)
+ def print_rc: String = Process_Result.print_rc(rc)
+
def print: Process_Result =
{
Output.warning(err)
--- a/src/Pure/Tools/phabricator.scala Sun Apr 12 21:53:58 2020 +0100
+++ b/src/Pure/Tools/phabricator.scala Mon Apr 13 16:16:22 2020 +0200
@@ -162,7 +162,7 @@
else {
val config = get_config(name)
val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true)
- if (!result.ok) error("Return code: " + result.rc.toString)
+ if (!result.ok) error(result.print_return_code)
}
})
--- a/src/Pure/Tools/server.scala Sun Apr 12 21:53:58 2020 +0100
+++ b/src/Pure/Tools/server.scala Mon Apr 13 16:16:22 2020 +0200
@@ -534,7 +534,7 @@
for ((_, session) <- sessions) {
try {
val result = session.stop()
- if (!result.ok) log("Session shutdown failed: return code " + result.rc)
+ if (!result.ok) log("Session shutdown failed: " + result.print_rc)
}
catch { case ERROR(msg) => log("Session shutdown failed: " + msg) }
}
--- a/src/Pure/Tools/server_commands.scala Sun Apr 12 21:53:58 2020 +0100
+++ b/src/Pure/Tools/server_commands.scala Mon Apr 13 16:16:22 2020 +0200
@@ -86,7 +86,10 @@
}))
if (results.ok) (results_json, results, options, base_info)
- else throw new Server.Error("Session build failed: return code " + results.rc, results_json)
+ else {
+ throw new Server.Error("Session build failed: " + Process_Result.print_rc(results.rc),
+ results_json)
+ }
}
}
@@ -136,7 +139,7 @@
val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)
if (result.ok) (result_json, result)
- else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json)
+ else throw new Server.Error("Session shutdown failed: " + result.print_rc, result_json)
}
}
--- a/src/Tools/VSCode/src/server.scala Sun Apr 12 21:53:58 2020 +0100
+++ b/src/Tools/VSCode/src/server.scala Mon Apr 13 16:16:22 2020 +0200
@@ -333,7 +333,8 @@
delay_preview.revoke()
val result = session.stop()
- if (result.ok) reply("") else reply("Prover shutdown failed: return code " + result.rc)
+ if (result.ok) reply("")
+ else reply("Prover shutdown failed: " + result.rc)
None
case None =>
reply("Prover inactive")
--- a/src/Tools/jEdit/src/session_build.scala Sun Apr 12 21:53:58 2020 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Mon Apr 13 16:16:22 2020 +0200
@@ -171,7 +171,7 @@
(Output.error_message_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
}
- progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
+ progress.echo(out + (if (rc == 0) "OK" else Process_Result.print_return_code(rc)) + "\n")
if (rc == 0) JEdit_Sessions.session_start(options)
else progress.echo("Session build failed -- prover process remains inactive!")