From f662f51467189da2d3a5cf7849b12c05fc5f0925 Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Tue, 14 Nov 2017 12:09:14 +1100 Subject: [PATCH] Remove refresh link, add refresh option to worker Reverts commit 900054ab6e61482508a7c6dd736a171696213398, then adds more. --- apiLib.sml | 1 + server.sml | 7 ++----- serverLib.sml | 1 - worker.sml | 6 +++++- 4 files changed, 8 insertions(+), 7 deletions(-) diff --git a/apiLib.sml b/apiLib.sml index 85b97b3..d922278 100644 --- a/apiLib.sml +++ b/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" diff --git a/server.sml b/server.sml index d353b05..201486f 100644 --- a/server.sml +++ b/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 diff --git a/serverLib.sml b/serverLib.sml index 1d60fdb..3cceebf 100644 --- a/serverLib.sml +++ b/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"]] diff --git a/worker.sml b/worker.sml index f331d74..58f360f 100644 --- a/worker.sml +++ b/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 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."];