[gui] restore property panel in absence of dgraph

only the graph dependencies window is replaced by a dialog indicating
that it is not available

Makefile

@@ -30,7 +30,8 @@ include share/Makefile.dynamic_config.internal
 
 #Check share/Makefile.config available
 ifndef FRAMAC_ROOT_SRCDIR
-$(error "You should run ./configure first (or autoconf if there is no configure)")
+$(error \
+  "You should run ./configure first (or autoconf if there is no configure)")
 endif
 
 ###################
@@ -99,7 +100,8 @@ DEFAULT_HEADER_DIRS := headers
 DEFAULT_HEADER_EXCEPTIONS := configure
 # default value used for CEA_PROPRIETARY_FILES and PLUGIN_CEA_PROPRIETARY_FILES
 DEFAULT_CEA_PROPRIETARY_FILES := tests/non-free/%
-# default value used for CEA_PROPRIETARY_HEADERS and PLUGIN_CEA_PROPRIETARY_HEADERS
+# default value used for CEA_PROPRIETARY_HEADERS
+# and PLUGIN_CEA_PROPRIETARY_HEADERS
 DEFAULT_CEA_PROPRIETARY_HEADERS := CEA_PROPRIETARY
 
 MERLIN_PACKAGES:=
@@ -306,7 +308,11 @@ DISTRIB_FILES:=\
 
 # Test files to be included in the distribution (without header checking).
 # Plug-ins should use PLUGIN_DISTRIB_TESTS to export their test files. 
-DISTRIB_TESTS=$(shell git ls-files tests src/plugins/aorai/tests src/plugins/report/tests src/plugins/wp/tests)
+DISTRIB_TESTS=$(shell git ls-files \
+                  tests \
+                  src/plugins/aorai/tests \
+                  src/plugins/report/tests \
+                  src/plugins/wp/tests)
 
 
 # files that are needed to compile API documentation of external plugins
@@ -349,7 +355,8 @@ rebuild: config.status
 		 $(MAKE) depend $(FRAMAC_PARALLEL) && \
 		 $(MAKE) all $(FRAMAC_PARALLEL))
 
-sinclude .Makefile.user # Should defines FRAMAC_PARALLEL, FRAMAC_USER_FLAGS, FRAMAC_USER_MERLIN_FLAGS
+sinclude .Makefile.user
+# Should define FRAMAC_PARALLEL, FRAMAC_USER_FLAGS, FRAMAC_USER_MERLIN_FLAGS
 
 #Create link in share for local execution if
 .PHONY:create_share_link
@@ -700,7 +707,8 @@ src/plugins/gui/GSourceView.mli: src/plugins/gui/GSourceView2.mli.in
 endif
 
 SOURCEVIEWCOMPAT:=GSourceView
-GENERATED+=src/plugins/gui/GSourceView.ml src/plugins/gui/GSourceView.mli
+GENERATED+=src/plugins/gui/GSourceView.ml src/plugins/gui/GSourceView.mli \
+           src/plugins/gui/dgraph_helper.ml src/plugins/gui/gtk_compat.ml
 
 ifeq ($(LABLGTK),lablgtk3)
 src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.3.ml
@@ -714,9 +722,15 @@ endif
 GENERATED+=src/plugins/gui/gtk_compat.ml
 
 ifeq ($(HAS_DGRAPH),yes)
-  DGRAPHFILES:=debug_manager property_navigator
+  DGRAPHFILES:=debug_manager
+  src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.yes.ml
+	$(CP) $< $@
+	$(CHMOD_RO) $@
 else
   DGRAPHFILES:=
+  src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.no.ml
+	$(CP) $< $@
+	$(CHMOD_RO) $@
 endif
 
 SINGLE_GUI_CMO:= \
@@ -726,6 +740,7 @@ SINGLE_GUI_CMO:= \
 	$(SOURCEVIEWCOMPAT) \
 	gui_parameters \
 	gtk_helper \
+        dgraph_helper \
         gtk_form \
 	source_viewer pretty_source source_manager book_manager \
 	warning_manager \
@@ -737,7 +752,8 @@ SINGLE_GUI_CMO:= \
 	design \
 	analyses_manager file_manager project_manager \
 	help_manager \
-        $(DGRAPHFILES)
+        $(DGRAPHFILES) \
+        property_navigator \
 
 SINGLE_GUI_CMO:= $(patsubst %,src/plugins/gui/%.cmo,$(SINGLE_GUI_CMO))
 

src/plugins/gui/dgraph_helper.no.ml

+let window_msg_unavailable () =
+  let buttons = GWindow.Buttons.ok in
+  let message_type = `WARNING in
+  let message =
+    "Frama-C has not been compiled against a library with \
+     working graph visualization. Property dependencies graph can't be shown."
+  in
+  ignore (GWindow.message_dialog ~buttons ~message_type ~message ())
+
+let graph_window ~parent:_ ~title:_ _ =
+  window_msg_unavailable ()
+
+let graph_window_through_dot ~parent:_ ~title:_ _ =
+  window_msg_unavailable ()

src/plugins/gui/dgraph_helper.yes.ml

+let graph_window ~parent ~title make_view =
+  let height = int_of_float (float parent#default_height *. 3. /. 4.) in
+  let width = int_of_float (float parent#default_width *. 3. /. 4.) in
+  let graph_window =
+    GWindow.window
+      ~width ~height ~title ~resizable:true ~position:`CENTER ()
+  in
+  let view = make_view ~packing:graph_window#add () in
+  graph_window#show();
+  view#adapt_zoom();
+  ()
+;;
+
+let graph_window_through_dot ~parent ~title dot_formatter =
+  let make_view ~packing () =
+    let temp_file =
+      try
+        Extlib.temp_file_cleanup_at_exit
+          "framac_property_status_navigator_graph" "dot"
+      with Extlib.Temp_file_error s ->
+        Gui_parameters.abort "cannot create temporary file: %s" s in
+    let fmt = Format.formatter_of_out_channel (open_out temp_file) in
+    dot_formatter fmt;
+    Format.pp_print_flush fmt ();
+    let view =
+      snd
+        (Dgraph.DGraphContainer.Dot.from_dot_with_commands ~packing temp_file)
+    in
+    view
+  in
+  try
+    graph_window ~parent ~title make_view
+  with Dgraph.DGraphModel.DotError _ as exn ->
+    Gui_parameters.error
+      "@[cannot display dot graph:@ %s@]"
+      (Printexc.to_string exn)

src/plugins/gui/property_navigator.ml

@@ -554,7 +554,8 @@ let make_panel (main_ui:main_window_extension_points) =
            | Some { MODEL.finfo = { ip = ip } } ->
                let format_graph ppf =
                  Consolidation_graph.dump (Consolidation_graph.get ip) ppf in
-               Gtk_helper.graph_window_through_dot main_ui#main_window "Dependencies" format_graph
+               Dgraph_helper.graph_window_through_dot
+                 main_ui#main_window "Dependencies" format_graph
            | None -> ()));
   view#selection#set_select_function
     (fun path currently_selected ->