[GUI] don't compile files that depend upon DGraph in lablgtk3

.gitignore

@@ -205,3 +205,5 @@ hello-*.tar.gz
 /src/plugins/gui/GSourceView.ml
 /src/plugins/gui/GSourceView.mli
 /tests/crowbar/integer_bb_pretty
+/src/plugins/gui/dgraph_helper.ml
+/doc/doxygen

Makefile

@@ -702,19 +702,6 @@ endif
 SOURCEVIEWCOMPAT:=GSourceView
 GENERATED+=src/plugins/gui/GSourceView.ml src/plugins/gui/GSourceView.mli
 
-DGRAPHCOMPAT:=
-ifeq ($(HAS_GNOMECANVAS),no)
-DGRAPHCOMPAT:=dgraph
-src/plugins/gui/dgraph.ml: src/plugins/gui/dgraph.ml.in
-	$(CP) $< $@
-	$(CHMOD_RO) $@
-src/plugins/gui/dgraph.mli: src/plugins/gui/dgraph.mli.in
-	$(CP) $< $@
-	$(CHMOD_RO) $@
-
-GENERATED+=src/plugins/gui/dgraph.ml src/plugins/gui/dgraph.mli
-endif
-
 ifeq ($(LABLGTK),lablgtk3)
 src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.3.ml
 	$(CP) $< $@
@@ -726,14 +713,20 @@ src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.2.ml
 endif
 GENERATED+=src/plugins/gui/gtk_compat.ml
 
+ifeq ($(HAS_DGRAPH),yes)
+  DGRAPHFILES:=debug_manager property_navigator
+else
+  DGRAPHFILES:=
+endif
+
 SINGLE_GUI_CMO:= \
 	wutil_once \
 	gtk_compat \
 	$(WTOOLKIT) \
 	$(SOURCEVIEWCOMPAT) \
-	$(DGRAPHCOMPAT) \
 	gui_parameters \
-	gtk_helper gtk_form \
+	gtk_helper \
+        gtk_form \
 	source_viewer pretty_source source_manager book_manager \
 	warning_manager \
 	filetree \
@@ -742,9 +735,9 @@ SINGLE_GUI_CMO:= \
 	history \
 	gui_printers \
 	design \
-	analyses_manager file_manager project_manager debug_manager \
+	analyses_manager file_manager project_manager \
 	help_manager \
-	property_navigator
+        $(DGRAPHFILES)
 
 SINGLE_GUI_CMO:= $(patsubst %,src/plugins/gui/%.cmo,$(SINGLE_GUI_CMO))
 
@@ -1052,9 +1045,10 @@ PLUGIN_ENABLE:=$(ENABLE_IMPACT)
 PLUGIN_NAME:=Impact
 PLUGIN_DIR:=src/plugins/impact
 PLUGIN_CMO:= options pdg_aux reason_graph compute_impact register
+ifeq ($(HAS_DGRAPH),yes)
 PLUGIN_GUI_CMO:= register_gui
+endif
 PLUGIN_DISTRIBUTED:=yes
-# PLUGIN_UNDOC:=impact_gui.ml
 PLUGIN_INTERNAL_TEST:=yes
 PLUGIN_DEPENDENCIES:=Inout Eva Pdg Slicing
 

src/plugins/gui/dgraph.mli.in

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2019                                               *)
-(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
-(*         alternatives)                                                  *)
-(*                                                                        *)
-(*  you can redistribute it and/or modify it under the terms of the GNU   *)
-(*  Lesser General Public License as published by the Free Software       *)
-(*  Foundation, version 2.1.                                              *)
-(*                                                                        *)
-(*  It is distributed in the hope that it will be useful,                 *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
-(*  GNU Lesser General Public License for more details.                   *)
-(*                                                                        *)
-(*  See the GNU Lesser General Public License version 2.1                 *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* dgraph module that always generates an error: Dgraph is not available
-   with gtk3
-*)
-
-module DGraphModel: sig
-  exception DotError of string
-end
-
-module DGraphContainer: sig
-
-  type status = Global | Tree | Both
-
-  module Dot: sig
-    val from_dot_with_commands:
-      ?packing:(GObj.widget ->unit) ->
-      ?status:status ->
-      string ->
-        GPack.table * <adapt_zoom: unit -> unit>
-  end
-end

src/plugins/gui/dgraph.ml.in → src/plugins/gui/dgraph_helper.mli

@@ -20,19 +20,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* dgraph module that always generates an error: Dgraph is not available
-   with gtk3
-*)
+(** Create a new window displaying a graph.
+    @plugin development guide *)
+val graph_window:
+  parent: GWindow.window ->
+  title:string ->
+  (packing:(GObj.widget -> unit) -> unit ->
+   <adapt_zoom: unit -> unit; ..>) ->
+  unit
 
-module DGraphModel = struct
-  exception DotError of string
-end
-
-module DGraphContainer = struct
-  type status = Global | Tree | Both
-
-  module Dot = struct
-    let from_dot_with_commands ?packing:_ ?status:_ _ =
-      raise (DGraphModel.DotError "DGraph is unsupported in GTK3")
-  end
-end
+(** Create a new window displaying a graph, by printing dot commands. *)
+val graph_window_through_dot:
+  parent: GWindow.window ->
+  title:string ->
+  (Format.formatter -> unit) ->
+  unit

src/plugins/gui/gtk_helper.ml

@@ -1014,44 +1014,6 @@ let spawn_command ?(timeout=0) ?stdout ?stderr s args f =
   let prio = Glib.int_of_priority `LOW in
   ignore (Glib.Idle.add ~prio for_idle)
 
-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)
-;;
-
 let image_menu_item ~(image:GObj.widget) ~text ~packing =
   let mi = GMenu.menu_item () in
   let box =

src/plugins/gui/gtk_helper.mli

@@ -426,22 +426,6 @@ val input_string :
     parent: GWindow.window -> title:string ->
     ?ok:string -> ?cancel:string -> ?text:string -> string -> string option
 
-(** Create a new window displaying a graph.
-    @plugin development guide *)
-val graph_window:
-  parent: GWindow.window ->
-  title:string ->
-  (packing:(GObj.widget -> unit) -> unit ->
-   <adapt_zoom: unit -> unit; ..>) ->
-  unit
-
-(** Create a new window displaying a graph, by printing dot commands. *)
-val graph_window_through_dot:
-  parent: GWindow.window ->
-  title:string ->
-  (Format.formatter -> unit) ->
-  unit
-
 (** calls the packing function to append a new menu item
     with an icon and a label.
     replaces GMenu.image_menu_item that has been deprecated in GTK3