diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 58509ea7812b062255854969fd52036d0a47c8f5..3878bb45f6376a737ff3be5c3030744338358c4c 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -1101,9 +1101,10 @@ let warn_error exn =
let with_progress ?debounced ?on_delayed trigger job data =
let d = on_progress ?debounced ?on_delayed trigger in
let result =
- try job data with e ->
+ try job data
+ with exn ->
off_progress d ;
- raise e
+ raise exn
in
off_progress d ; result
@@ -1112,7 +1113,7 @@ let with_progress ?debounced ?on_delayed trigger job data =
let canceled = ref false
let cancel () = canceled := true
-let fire ~delayed ~forced ~time d =
+let fire ~warn_on_delayed ~forced ~time d =
if forced || time > d.next_at then
begin
try
@@ -1125,7 +1126,7 @@ let fire ~delayed ~forced ~time d =
match d.on_delayed with
| None -> ()
| Some warn ->
- if delayed && 0.0 < d.last_yield_at then
+ if warn_on_delayed && 0.0 < d.last_yield_at then
begin
let time_since_last_yield = time -. d.last_yield_at in
let delay = if d.debounced > 0.0 then d.debounced else 0.1 in
@@ -1139,18 +1140,18 @@ let raise_if_canceled () =
(* ---- Yielding ---- *)
-let do_yield ~delayed ~forced () =
+let do_yield ~warn_on_delayed ~forced () =
match !daemons with
| [] -> ()
| ds ->
begin
let time = Unix.gettimeofday () in
- List.iter (fire ~delayed ~forced ~time) ds ;
+ List.iter (fire ~warn_on_delayed ~forced ~time) ds ;
raise_if_canceled () ;
end
-let yield = do_yield ~delayed:true ~forced:false
-let flush = do_yield ~delayed:false ~forced:true
+let yield = do_yield ~warn_on_delayed:true ~forced:false
+let flush = do_yield ~warn_on_delayed:false ~forced:true
(* ---- Sleeping ---- *)
@@ -1167,23 +1168,24 @@ let sleep ms =
if period = 0 then
begin
Unix.sleepf delta ;
- do_yield ~delayed:false ~forced:false ()
+ do_yield ~warn_on_delayed:false ~forced:false ()
end
else
let delay = float period *. 0.001 in
let finished_at = Unix.gettimeofday () +. delta in
let rec wait_and_trigger () =
- begin
- Unix.sleepf delay ;
- let time = Unix.gettimeofday () in
- List.iter (fire ~delayed:false ~forced:false ~time) !daemons ;
- raise_if_canceled () ;
- if time < finished_at then
- if time +. delay > finished_at then
- Unix.sleepf (finished_at -. time)
- else wait_and_trigger ()
- end
- in wait_and_trigger ()
+ Unix.sleepf delay ;
+ let time = Unix.gettimeofday () in
+ List.iter
+ (fire ~warn_on_delayed:false ~forced:false ~time)
+ !daemons ;
+ raise_if_canceled () ;
+ if time < finished_at then
+ if time +. delay > finished_at then
+ Unix.sleepf (finished_at -. time)
+ else wait_and_trigger ()
+ in
+ wait_and_trigger ()
(* ---- Deprecated old API ---- *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 81a619eb97ead133448298519da8049dcbce8aa7..6f1fde19394999143e722f43d644a403928cdb2b 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -1339,17 +1339,18 @@ module Derefs : INOUT with type t = Locations.Zone.t
@plugin development guide
@deprecated Frama-C+dev *)
val progress: (unit -> unit) ref
+[@@ deprecated "Use {!yield} instead"]
(** Registered daemon on progress. *)
type daemon
(**
[on_progress ?debounced ?on_delayed trigger] registers [trigger] as new
- daemon to be executed on each [yield].
- @param debounced the least amount of time, in milliseconds, between two
- successive calls to the daemon (default is 0ms).
+ daemon to be executed on each {!yield}.
+ @param debounced the least amount of time between two successive calls to the
+ daemon, in milliseconds (default is 0ms).
@param on_delayed the callback invoked as soon as the time since the last
- [yield] is greater than [debounced] milliseconds (or 100ms at least).
+ {!yield} is greater than [debounced] milliseconds (or 100ms at least).
*)
val on_progress :
?debounced:int -> ?on_delayed:(int -> unit) -> (unit -> unit) -> daemon
@@ -1360,11 +1361,13 @@ val off_progress : daemon -> unit
(** Trigger all daemons immediately. *)
val flush : unit -> unit
-(** Trigger all registered daemons (debounced). *)
+(** Trigger all registered daemons (debounced).
+ This function should be called from time to time by all analysers taking
+ time. In GUI mode, this will make the interface reactive. *)
val yield : unit -> unit
-(** Interrupt the currently running job.
- The next call to [Db.yield()] will raise a [Cancel] exception. *)
+(** Interrupt the currently running job at the next call to {!yield} as a
+ [Cancel] exception is raised. *)
val cancel : unit -> unit
(**
@@ -1405,7 +1408,7 @@ val with_progress :
*)
val sleep : int -> unit
-(** This exception may be raised by {!progress} to interrupt computations. *)
+(** This exception may be raised by {!yield} to interrupt computations. *)
exception Cancel
(*
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index 61abedfbde25ad1583cecdb498eac892d989a09d..fc42c15e056be1317b6ed6add87a493eb60e691f 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -26,7 +26,6 @@
module Senv = Server_parameters
-let option f = function None -> () | Some x -> f x
(* -------------------------------------------------------------------------- *)
(* --- Registry --- *)
@@ -181,7 +180,7 @@ let process_request (server : 'a server) (request : 'a request) : unit =
| `Poll -> ()
| `Shutdown ->
begin
- option kill_exec server.running ;
+ Extlib.may kill_exec server.running ;
Queue.clear server.q_in ;
Stack.clear server.q_out ;
server.shutdown <- true ;
@@ -190,7 +189,7 @@ let process_request (server : 'a server) (request : 'a request) : unit =
begin
let set_killed = kill_request server.equal id in
Queue.iter set_killed server.q_in ;
- option set_killed server.running ;
+ Extlib.may set_killed server.running ;
end
| `Request(id,request,data) ->
begin
@@ -227,17 +226,15 @@ let communicate server =
Stack.iter (fun r -> pool := r :: !pool) server.q_out ;
Stack.clear server.q_out ;
message.callback !pool ;
- option raise error ; true
+ Extlib.may raise error ; true
(* -------------------------------------------------------------------------- *)
(* --- Yielding --- *)
(* -------------------------------------------------------------------------- *)
let do_yield server () =
- begin
- option raise_if_killed server.running ;
- ignore ( communicate server );
- end
+ Extlib.may raise_if_killed server.running ;
+ ignore ( communicate server )
(* -------------------------------------------------------------------------- *)
(* --- One Step Process --- *)
@@ -265,10 +262,10 @@ let in_range ~min:a ~max:b v = min (max a v) b
let kill () = raise Killed
-let demons = ref []
-let on callback = demons := !demons @ [ callback ]
+let daemons = ref []
+let on callback = daemons := !daemons @ [ callback ]
let signal activity =
- List.iter (fun f -> try f activity with _ -> ()) !demons
+ List.iter (fun f -> try f activity with _ -> ()) !daemons
let create ~pretty ?(equal=(=)) ~fetch () =
let polling = in_range ~min:1 ~max:200 (Senv.Polling.get ()) in
@@ -287,36 +284,38 @@ let create ~pretty ?(equal=(=)) ~fetch () =
let start server =
match server.daemon with
- | Some _db -> ()
+ | Some _ -> ()
| None ->
begin
Senv.feedback "Server enabled." ;
- let db = Db.on_progress
+ let daemon =
+ Db.on_progress
~debounced:server.polling
?on_delayed:(delayed "command line")
- (do_yield server) in
- server.daemon <- Some db ;
+ (do_yield server)
+ in
+ server.daemon <- Some daemon ;
signal true ;
end
let stop server =
match server.daemon with
| None -> ()
- | Some db ->
+ | Some daemon ->
begin
Senv.feedback "Server disabled." ;
server.daemon <- None ;
- Db.off_progress db ;
+ Db.off_progress daemon ;
signal false ;
end
let foreground server =
match server.daemon with
| None -> ()
- | Some db ->
+ | Some daemon ->
begin
server.daemon <- None ;
- Db.off_progress db ;
+ Db.off_progress daemon ;
end
(* -------------------------------------------------------------------------- *)
@@ -331,7 +330,8 @@ let run server =
Senv.feedback "Server running." ;
foreground server ;
signal true ;
- begin try
+ begin
+ try
while not server.shutdown do
let activity = process server in
if not activity then Db.sleep server.polling
diff --git a/src/plugins/server/main.mli b/src/plugins/server/main.mli
index c6f1b7d9f1496ff6fa80e8bf02aafcbe869647a2..4c4da8678f190aa2c6ec5180c030b9a5d67cec59 100644
--- a/src/plugins/server/main.mli
+++ b/src/plugins/server/main.mli
@@ -83,13 +83,13 @@ val create :
fetch:(unit -> 'a message option) ->
unit -> 'a server
-(** Run the server forever *)
+(** Run the server forever. *)
val run : 'a server -> unit
-(** Start the server in background *)
+(** Start the server in background. *)
val start : 'a server -> unit
-(** Stop the server if it is running in background *)
+(** Stop the server if it is running in background. *)
val stop : 'a server -> unit
(** Kills the currently running request. Actually raises an exception. *)
diff --git a/src/plugins/server/server_parameters.ml b/src/plugins/server/server_parameters.ml
index cfd45c6e626e78d0831922dd8a1f9fbcc79ad3eb..5b9e0018622e06add5fcf012e2bdc76d0d0d92cc 100644
--- a/src/plugins/server/server_parameters.ml
+++ b/src/plugins/server/server_parameters.ml
@@ -42,13 +42,14 @@ module Polling = P.Int
let option_name = "-server-polling"
let arg_name = "ms"
let default = 50
- let help = "Server polling (in milliseconds, default 50ms)"
+ let help = "Server polling time period, in milliseconds (default 50ms)"
end)
module AutoLog = P.False
(struct
let option_name = "-server-auto-log"
- let help = "Start monitoring logs before server is running (default is false)"
+ let help =
+ "Start monitoring logs before server is running (default is false)"
end)
(* -------------------------------------------------------------------------- *)