diff --git a/.gitignore b/.gitignore
index 633a7d72b4f6a96980eec0d1d508467a17ddfa92..4a02282acf004d3b931b47a2a0979ec39c846a98 100644
--- a/.gitignore
+++ b/.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
diff --git a/Makefile b/Makefile
index 90e779f26d5e8b41b527d0d974ff726fedb5e349..5e6dc25df8a77673e548daaac88526252dd28f0a 100644
--- a/Makefile
+++ b/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
diff --git a/src/plugins/gui/dgraph.mli.in b/src/plugins/gui/dgraph.mli.in
deleted file mode 100644
index 5cf0b53f22586ca29745199c4b73efdbd7401939..0000000000000000000000000000000000000000
--- a/src/plugins/gui/dgraph.mli.in
+++ /dev/null
@@ -1,42 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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
diff --git a/src/plugins/gui/dgraph.ml.in b/src/plugins/gui/dgraph_helper.mli
similarity index 79%
rename from src/plugins/gui/dgraph.ml.in
rename to src/plugins/gui/dgraph_helper.mli
index f672460d995880f279523fed4cc47a9e9b3625a3..632035356b8644aace00e2b837cf568565b0285c 100644
--- a/src/plugins/gui/dgraph.ml.in
+++ b/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
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 0c3551ccbb0663fc2a0859f8a2c8561377f999f7..24f8b32bd9b57253fcc8bffd85fe726c751c6ad8 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/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 =
diff --git a/src/plugins/gui/gtk_helper.mli b/src/plugins/gui/gtk_helper.mli
index 6d9d605b34bf5dd4da7058b20f071f786cbb47f5..c07246254458ee9ab58d18160fa79967b68dd951 100644
--- a/src/plugins/gui/gtk_helper.mli
+++ b/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