From 29485e412cf255f3f20b07a91813bda49e0b3b4c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 27 Jan 2020 11:48:34 +0100
Subject: [PATCH] [server] launch gui
---
bin/frama-c-zmq | 2 +
src/plugins/server/main.ml | 10 +++-
src/plugins/server/server_zmq.ml | 88 ++++++++++++++++++++++++--------
3 files changed, 76 insertions(+), 24 deletions(-)
create mode 100755 bin/frama-c-zmq
diff --git a/bin/frama-c-zmq b/bin/frama-c-zmq
new file mode 100755
index 00000000000..a3a8d7179e4
--- /dev/null
+++ b/bin/frama-c-zmq
@@ -0,0 +1,2 @@
+#!/bin/sh
+echo "ZMQ Client *@"
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index 0a829101064..7528d3552ae 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -330,13 +330,19 @@ let run server =
let idle_s = float_of_int idle_ms /. 1000.0 in
while not server.shutdown do
let activity = process server in
- if not activity then Unix.sleepf idle_s ;
+ if not activity then
+ begin
+ Unix.sleepf idle_s ;
+ !Db.progress () ;
+ end
done ;
with Sys.Break -> () (* Ctr+C, just leave the loop normally *)
end;
Senv.feedback "Server shutdown." ;
signal false ;
- with exn ->
+ with
+ | Killed -> ()
+ | exn ->
Senv.feedback "Server interruped (fatal error)." ;
signal false ;
raise exn
diff --git a/src/plugins/server/server_zmq.ml b/src/plugins/server/server_zmq.ml
index cb940de721d..b428bc39021 100644
--- a/src/plugins/server/server_zmq.ml
+++ b/src/plugins/server/server_zmq.ml
@@ -47,6 +47,12 @@ module Run = Senv.Action
let help = "Launch the ZeroMQ server (until shutdown)."
end)
+module Gui = Senv.Action
+ (struct
+ let option_name = "-server-gui"
+ let help = "Launch the external GUI."
+ end)
+
let _ = Doc.page `Protocol ~title:"ZeroMQ Protocol" ~filename:"server_zmq.md"
(* -------------------------------------------------------------------------- *)
@@ -60,7 +66,7 @@ let zmq_context =
| Some ctxt -> ctxt
| None ->
let major,minor,patch = Zmq.version () in
- Senv.feedback "ZeroMQ [v%d.%d.%d]" major minor patch ;
+ Senv.debug "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
@@ -125,32 +131,70 @@ let fetch socket () =
(* -------------------------------------------------------------------------- *)
let pretty = Format.pp_print_string
-let background = ref None
+let server = ref None
+let client = ref None
+
+let ping () =
+ match !client with None -> None | Some process ->
+ try Some (process ())
+ with Unix.Unix_error _ -> None
+
+let temp_url () =
+ let socket = Filename.temp_file "frama-c.socket" ".io" in
+ Extlib.safe_at_exit (fun () -> Extlib.safe_remove socket) ;
+ "ipc://" ^ socket
+
+let launch_client url server =
+ match !client with
+ | Some _ -> ()
+ | None ->
+ begin
+ let cmd = Filename.dirname Sys.argv.(0) ^ "/frama-c-zmq" in
+ let process = Command.command_async cmd [| "--connect" ; url |] in
+ Senv.debug "%s --connect %s@." cmd url ;
+ Senv.feedback "Client launched." ;
+ client := Some process ;
+ Extlib.safe_at_exit
+ begin fun () ->
+ match ping () with
+ | Some (Not_ready kill) ->
+ Senv.feedback "Client interrupted." ;
+ kill ()
+ | _ -> ()
+ end ;
+ Main.start server ;
+ Cmdline.at_normal_exit (fun () -> Main.run server);
+ end
+
+let establish url =
+ let context = zmq_context () in
+ let socket = Zmq.Socket.(create context rep) in
+ try
+ Zmq.Socket.bind socket url ;
+ Senv.debug "ZeroMQ [%s]" url ;
+ let srv = Main.create ~pretty ~fetch:(fetch socket) () in
+ server := Some(url,srv) ;
+ Extlib.safe_at_exit begin fun () ->
+ Main.stop srv ;
+ Zmq.Socket.close socket ;
+ server := None ;
+ end ;
+ if Gui.get () then launch_client url srv else
+ if Run.get () then Main.run srv else Main.start srv ;
+ with exn ->
+ Zmq.Socket.close socket ;
+ raise exn
let cmdline () =
begin
- match !background with
- | Some server ->
- if Run.get () then Main.run server
+ match !server with
+ | Some(url,srv) ->
+ if Gui.get () then launch_client url srv else
+ if Run.get () then Main.run srv
| None ->
let url = Socket.get () in
- if url <> "" then
- let context = zmq_context () in
- 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 () ->
- Main.stop server ;
- Zmq.Socket.close socket ;
- background := None ;
- end ;
- if Run.get () then Main.run server else Main.start server ;
- with exn ->
- Zmq.Socket.close socket ;
- raise exn
+ if url <> "" then establish url else
+ if Gui.get () then establish (temp_url())
end
let () = Db.Main.extend cmdline
--
GitLab