Just a style rework.

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 ---- *)
 

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
 
 (*

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

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. *)

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)
 
 (* -------------------------------------------------------------------------- *)