Remove refresh link, add refresh option to worker

Reverts commit 900054a, then adds more.

apiLib.sml

@@ -85,6 +85,7 @@ datatype api = Waiting | Refresh
              | Append of id * line (* not including newline *)
              | Stop of id | Abort of id
 
+val refresh_response = "refreshed\n"
 val claim_response = "claimed\n"
 val append_response = "appended\n"
 val stop_response = "stopped\n"

server.sml

@@ -173,19 +173,16 @@ fun get_api () =
 local
   fun id_list ids = String.concatWith " " (List.map Int.toString ids)
 in
-  fun dispatch Refresh =
-    ((refresh (); TextIO.output(TextIO.stdOut,String.concat["Location:",base_url,"\n\n"]))
-     handle e => cgi_die [exnMessage e])
-  | dispatch api =
+  fun dispatch api =
     text_response (
       case api of
         Waiting => id_list (waiting())
+      | Refresh => (refresh (); refresh_response)
       | Job id => file_to_string (job id)
       | Claim(id,name) => (claim id name; claim_response)
       | Append(id,line) => (append id line; append_response)
       | Stop id => (stop id; stop_response)
       | Abort id => (abort id; abort_response)
-      | Refresh => raise(Fail"impossible")
     ) handle e => cgi_die [exnMessage e]
 end
 

serverLib.sml

@@ -755,7 +755,6 @@ in
          (queue_dirs,
           List.map (fn f => f()) queue_funs))
     @ [footer [a host "CakeML main page",
-               a (String.concat[base_url,"/api/refresh"]) "Refresh jobs from GitHub",
                a "https://github.com/CakeML/regression" "Site code on GitHub",
                a (String.concat["https://validator.w3.org/nu/?doc=",server]) "Valid HTML",
                a (String.concat["https://jigsaw.w3.org/css-validator/validator?uri=",server,style_href]) "Valid CSS"]]

worker.sml

@@ -31,7 +31,8 @@ fun usage_string name = String.concat[
   "                attempt to start running it again. If the job fails again,\n",
   "                exit (even without --no-loop).\n",
   "  --abort id  : Mark job <id> as having aborted, i.e., stopped without a proper\n",
-  "                success or failure, then exit.\n"];
+  "                success or failure, then exit.\n",
+  "  --refresh   : Refresh the server's waiting queue from GitHub then exit.\n"];
 
 (*
 
@@ -376,6 +377,9 @@ fun main () =
     val () = if List.exists (fn a => a="--help" orelse a="-h" orelse a="-?") args
              then (TextIO.output(TextIO.stdOut, usage_string(CommandLine.name())); OS.Process.exit OS.Process.success)
              else ()
+    val () = if List.exists (equal "--refresh") args
+             then (TextIO.output(TextIO.stdOut, API.send Refresh); OS.Process.exit OS.Process.success)
+             else ()
     val () = case get_int_arg "--abort" args of NONE => ()
              | SOME id => (
                  diag ["Marking job ",Int.toString id," as aborted."];