diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index 46c204d72366ee3e90f6160d5dbc61a078989eeb..796f4c54dce76dfcd7a8422f0e45706c55c44694 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -47,8 +47,21 @@ end
type 'a data = (module S with type t = 'a)
-let failure js msg =
- Pretty_utils.ksfprintf (fun msg -> raise(Ju.Type_error(msg,js))) msg
+exception InputError of string
+
+let failure ?json msg =
+ let add_json msg =
+ let msg = match json with
+ | None -> msg
+ | Some json ->
+ Format.asprintf "@[%s:@ %s@]" msg (Js.pretty_to_string json)
+ in
+ raise(InputError(msg))
+ in
+ Pretty_utils.ksfprintf add_json msg
+
+let failure_from_type_error msg json =
+ failure ~json "%s" msg
(* -------------------------------------------------------------------------- *)
(* --- Option --- *)
@@ -84,7 +97,7 @@ struct
let to_json (x,y) = `List [ A.to_json x ; B.to_json y ]
let of_json = function
| `List [ ja ; jb ] -> A.of_json ja , B.of_json jb
- | js -> failure js "Expected list with 2 elements"
+ | js -> failure ~json:js "Expected list with 2 elements"
end
module Jtriple(A : S)(B : S)(C : S) : S with type t = A.t * B.t * C.t =
@@ -94,7 +107,7 @@ struct
let to_json (x,y,z) = `List [ A.to_json x ; B.to_json y ; C.to_json z ]
let of_json = function
| `List [ ja ; jb ; jc ] -> A.of_json ja , B.of_json jb , C.of_json jc
- | js -> failure js "Expected list with 3 elements"
+ | js -> failure ~json:js "Expected list with 3 elements"
end
(* -------------------------------------------------------------------------- *)
@@ -354,7 +367,7 @@ struct
let id = Ju.to_int js in
try find m id
with Not_found ->
- failure js "[%s] No registered id #%d" I.name id
+ failure "[%s] No registered id #%d" I.name id
end
@@ -453,7 +466,7 @@ struct
let of_json js =
let k = Ju.to_int js in
try find k
- with Not_found -> failure js "[%s] No registered id #%d" A.name k
+ with Not_found -> failure "[%s] No registered id #%d" A.name k
end)
end
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
index f0c993fd042ca28c5abc2b961071ac01c9a4cb14..8c12a9465e4098629c4a1afd215439e31a481ef8 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -181,10 +181,16 @@ end
module Dictionary(E : Enum) : S_collection with type t = E.t
(* -------------------------------------------------------------------------- *)
-(** {2 Misc} *)
+(** {2 Error handling} *)
(* -------------------------------------------------------------------------- *)
-val failure : json -> ('a, Format.formatter, unit, 'b) format4 -> 'a
-(** @raise Yojson.Basic.Util.Type_error with provided message *)
+(** Exception thrown during the decoding of a request's inputs *)
+exception InputError of string
+
+val failure : ?json:json -> ('a, Format.formatter, unit, 'b) format4 -> 'a
+(** @raise InputError with provided message *)
+
+val failure_from_type_error : string -> json -> 'a
+(** @raise InputError from Yojson.Basic.Util.Type_error arguments *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 229c526ab6f75a73624235f3c09c42b5a4ed27e5..77605bf53f37fa4b3c2518de252644bcaa148c17 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -107,13 +107,14 @@ module Stmt = Data.Collection
~descr:(Md.rm "Code statement identifier") ()
let to_json st = `String (Tag.of_stmt st)
let of_json js =
+ let id = Js.to_string js in
try
let open Printer_tag in
- match Tag.lookup (Js.to_string js) with
+ match Tag.lookup id with
| PStmt(_,st) -> st
| _ -> raise Not_found
with Not_found ->
- Data.failure js "Unknown stmt id"
+ Data.failure "Unknown stmt id: '%s'" id
end)
module Ki = Data.Collection
@@ -137,8 +138,9 @@ module Kf = Data.Collection
let to_json kf =
`String (Kernel_function.get_name kf)
let of_json js =
- try Js.to_string js |> Globals.Functions.find_by_name
- with Not_found -> Data.failure js "Undefined function"
+ let key = Js.to_string js in
+ try Globals.Functions.find_by_name key
+ with Not_found -> Data.failure "Undefined function '%s'" key
end)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index 4cfd33596d14017a5ea0e0584435616387d44b84..7448c53e42df57194b8c9855689822507fb1e25a 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -78,7 +78,7 @@ struct
| `Assoc [ "file" , `String path ; "line" , `Int line ]
| `Assoc [ "line" , `Int line ; "file" , `String path ]
-> Log.source ~file:(Filepath.Normalized.of_string path) ~line
- | js -> failure js "Invalid source format"
+ | js -> failure_from_type_error "Invalid source format" js
end
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index 2602e89fe5f4b7cef908529ccf56db56f41dc3ad..c00a228cf41eeb502c18f4eb23bf1695d5deb581 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -134,24 +134,28 @@ let pp_response pp fmt (r : _ response) =
let no_yield () = ()
-let execute yield exec : _ response =
- let db = !Db.progress in
+let execute exec : _ response =
try
- Db.progress := if exec.yield then yield else no_yield ;
let data = exec.handler exec.data in
- Db.progress := db ; `Data(exec.id,data)
+ `Data(exec.id,data)
with
- | Killed -> Db.progress := db ; `Killed exec.id
- | exn ->
- Db.progress := db ;
+ | Killed -> `Killed exec.id
+ | Data.InputError msg -> `Error(exec.id,msg)
+ | Sys.Break as exn -> raise exn (* Silently pass the exception *)
+ | exn when Cmdline.catch_at_toplevel exn ->
Senv.warning "[%s] Uncaught exception:@\n%s"
exec.request (Cmdline.protect exn) ;
`Error(exec.id,Printexc.to_string exn)
+let execute_with_yield yield exec =
+ let db = !Db.progress in
+ Db.progress := if exec.yield then yield else no_yield ;
+ Extlib.try_finally ~finally:(fun () -> Db.progress := db) execute exec
+
let execute_debug pp yield exec =
if Senv.debug_atleast 1 then
Senv.debug "Trigger %s:%a" exec.request pp exec.id ;
- execute yield exec
+ execute_with_yield yield exec
let reply_debug server resp =
if Senv.debug_atleast 1 then
@@ -191,7 +195,7 @@ let process_request (server : 'a server) (request : 'a request) : unit =
| Some( `GET , handler ) ->
let exec = { id ; request ; handler ; data ;
yield = false ; killed = false } in
- reply_debug server (execute no_yield exec)
+ reply_debug server (execute exec)
| Some( `SET , handler ) ->
let exec = { id ; request ; handler ; data ;
yield = false ; killed = false } in
@@ -283,18 +287,24 @@ let run ~pretty ?(equal=(=)) ~fetch () =
shutdown = false ;
} in
try
+ (* TODO: remove the following line once the Why3 signal handler is not
+ used anymore. *)
+ Sys.catch_break true;
signal true ;
Senv.feedback "Server running." ;
- while not server.shutdown do
- let activity = process server in
- if not activity then Unix.sleepf idle_s ;
- done ;
+ begin try
+ while not server.shutdown do
+ let activity = process server in
+ if not activity then Unix.sleepf idle_s ;
+ done ;
+ with Sys.Break -> () (* Ctr+C, just leave the loop normally *)
+ end;
Senv.feedback "Server shutdown." ;
signal false ;
- with err ->
+ with exn ->
Senv.feedback "Server interruped (fatal error)." ;
signal false ;
- raise err
+ raise exn
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/request.ml b/src/plugins/server/request.ml
index b355b3907879b1e91eef4345b217d39680fb98bc..039ee9f3c3c161cc5fb5d7f9fa688b1f50b625ec 100644
--- a/src/plugins/server/request.ml
+++ b/src/plugins/server/request.ml
@@ -175,7 +175,7 @@ type ('a,'b) signature = {
}
let failure_missing fmap name =
- Data.failure (fmap_to_json fmap) "Missing parameter '%s'" name
+ Data.failure ~json:(fmap_to_json fmap) "Missing parameter '%s'" name
let check_required fmap fd =
if not (Fmap.mem fd fmap) then failure_missing fmap fd
@@ -276,9 +276,16 @@ let mk_input (type a) name defaults (input : a rq_input) : (rq -> json -> a) =
| Pnone -> Senv.fatal "No input defined for request '%s'" name
| Pdata d ->
let module D = (val d) in
- (fun rq js -> rq.result <- defaults ; D.of_json js)
+ begin fun rq js ->
+ rq.result <- defaults ;
+ try D.of_json js
+ with Jutil.Type_error (msg, js) -> Data.failure_from_type_error msg js
+ end
| Pfields _ ->
- (fun rq js -> rq.param <- fmap_of_json rq.param js)
+ begin fun rq js ->
+ try rq.param <- fmap_of_json rq.param js
+ with Jutil.Type_error (msg, js) -> Data.failure_from_type_error msg js
+ end
(* json output processing *)
let mk_output (type b) name required (output : b rq_output) : (rq -> b -> json) =