diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index af05488f599dbeb746a800ba05315730341010c6..119ba52b5e7b80404613ddc2c1977625d43be98e 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -185,12 +185,8 @@ let monitoring = ref false
let monitored = ref false
let events : Log.event Queue.t = Queue.create ()
-let monitor flag =
+let set_monitoring flag =
if flag != !monitoring then
- ( if flag then
- Senv.feedback "Start logs monitoring."
- else
- Senv.feedback "Stop logs monitoring." ) ;
monitoring := flag ;
if !monitoring && not !monitored then
begin
@@ -198,14 +194,19 @@ let monitor flag =
Log.add_listener (fun evt -> if !monitoring then Queue.add evt events)
end
-let monitor_logs () = monitor (Senv.Log.get ())
-
let monitor_server activity =
- if activity then monitor true else monitor_logs ()
+ if not (Senv.AutoLog.get ()) then set_monitoring activity
+
+let monitor_autologs () =
+ if Senv.AutoLog.get () then
+ begin
+ Senv.feedback "Auto-log started." ;
+ set_monitoring true ;
+ end
let () =
Main.on monitor_server ;
- Cmdline.run_after_configuring_stage monitor_logs
+ Cmdline.run_after_configuring_stage monitor_autologs
(* -------------------------------------------------------------------------- *)
(* --- Log Requests --- *)
@@ -214,7 +215,8 @@ let () =
let () = Request.register
~page ~kind:`SET ~name:"kernel.setLogs"
~descr:(Md.plain "Turn logs monitoring on/off")
- ~input:(module Jbool) ~output:(module Junit) monitor
+ ~input:(module Jbool) ~output:(module Junit)
+ set_monitoring
let () = Request.register
~page ~kind:`GET ~name:"kernel.getLogs"
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index 7749727054886a28ec102143c06f0b5c77bd3f4f..0a829101064217b7c52f514c2ace75b82751e3d9 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -286,8 +286,10 @@ let start server =
| Some _db -> ()
| None ->
begin
+ Senv.feedback "Server enabled." ;
let db = !Db.progress in
server.background <- Some db ;
+ signal true ;
Db.progress := do_yield server ;
end
@@ -296,11 +298,21 @@ let stop server =
| None -> ()
| Some db ->
begin
+ Senv.feedback "Server disabled." ;
server.background <- None ;
signal false ;
Db.progress := db ;
end
+let foreground server =
+ match server.background with
+ | None -> ()
+ | Some db ->
+ begin
+ server.background <- None ;
+ Db.progress := db ;
+ end
+
(* -------------------------------------------------------------------------- *)
(* --- Main Loop --- *)
(* -------------------------------------------------------------------------- *)
@@ -309,7 +321,7 @@ let run server =
try
(* TODO: remove the following line once the Why3 signal handler is not
used anymore. *)
- stop server ;
+ foreground server ;
Sys.catch_break true;
signal true ;
Senv.feedback "Server running." ;
diff --git a/src/plugins/server/server_parameters.ml b/src/plugins/server/server_parameters.ml
index 0b00960d594447f5c958d021b2c3191baef9dfeb..8ca2d009ce3a7e6d596db64f8e6093337c5c565a 100644
--- a/src/plugins/server/server_parameters.ml
+++ b/src/plugins/server/server_parameters.ml
@@ -53,9 +53,9 @@ module Yield = P.Int
let help = EXEC yield period (in milliseconds, default 50ms)"
end)
-module Log = P.False
+module AutoLog = P.False
(struct
- let option_name = "-server-logs"
+ let option_name = "-server-auto-log"
let help = "Start monitoring logs before server is running (default is false)"
end)
diff --git a/src/plugins/server/server_parameters.mli b/src/plugins/server/server_parameters.mli
index 9bbd8a148fde84d797559b9675f44098c42e59c7..9d3ef7e958d91fe67eb820aa09f79812d3e9c5b2 100644
--- a/src/plugins/server/server_parameters.mli
+++ b/src/plugins/server/server_parameters.mli
@@ -27,7 +27,7 @@ include Plugin.General_services
module Idle : Parameter_sig.Int (** Idle waiting time (in ms) *)
module Yield : Parameter_sig.Int (** Yield time (in ms) *)
module Doc : Parameter_sig.String (** Generate documentation *)
-module Log : Parameter_sig.Bool (** Monitor logs *)
+module AutoLog : Parameter_sig.Bool (** Monitor logs *)
val wpage : warn_category (** Inconsistent page warning *)
val wkind : warn_category (** Inconsistent category warning *)
diff --git a/src/plugins/server/server_zmq.ml b/src/plugins/server/server_zmq.ml
index 05a2b23d7ec84374a89befd72d42a2d8553c8c37..cb940de721d2e2dbd19b20584a0c5b33b8e8bb75 100644
--- a/src/plugins/server/server_zmq.ml
+++ b/src/plugins/server/server_zmq.ml
@@ -60,7 +60,7 @@ let zmq_context =
| Some ctxt -> ctxt
| None ->
let major,minor,patch = Zmq.version () in
- Senv.feedback "ZeroMQ %d.%d.%d" major minor patch ;
+ Senv.feedback "ZeroMQ [v%d.%d.%d]" major minor patch ;
let ctxt = Zmq.Context.create () in
at_exit (fun () -> Zmq.Context.terminate ctxt) ;
zmq := Some ctxt ; ctxt
@@ -139,23 +139,15 @@ let cmdline () =
let socket = Zmq.Socket.(create context rep) in
try
Zmq.Socket.bind socket url ;
+ Senv.feedback "ZeroMQ [%s]" url ;
let server = Main.create ~pretty ~fetch:(fetch socket) () in
background := Some server ;
at_exit begin fun () ->
- Senv.feedback "ZeroMQ [%s] stopped" url ;
+ Main.stop server ;
Zmq.Socket.close socket ;
background := None ;
end ;
- if Run.get () then
- begin
- Senv.feedback "ZeroMQ [%s] running" url ;
- Main.run server
- end
- else
- begin
- Senv.feedback "ZeroMQ [%s] started" url ;
- Main.start server
- end
+ if Run.get () then Main.run server else Main.start server ;
with exn ->
Zmq.Socket.close socket ;
raise exn