clarified signature;
authorwenzelm
Mon, 13 Apr 2020 16:16:22 +0200
changeset 71747 1dd514c8c1df
parent 71746 da0e18db1517
child 71748 34de8369c290
clarified signature;
src/Pure/PIDE/prover.scala
src/Pure/System/process_result.scala
src/Pure/Tools/phabricator.scala
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.scala
src/Tools/VSCode/src/server.scala
src/Tools/jEdit/src/session_build.scala
--- 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!")