diff --git a/.gitignore b/.gitignore
index 583b96d24e7700d71389dd6fa5ddfa759504e0b5..065769eeba111c28e7250e496aec936c81b7db4f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -197,3 +197,10 @@ hello-*.tar.gz
#######################
# should remain empty #
#######################
+/src/plugins/gui/GSourceView2.mli
+/src/plugins/gui/GSourceView2.ml
+/src/plugins/gui/dgraph.ml
+/src/plugins/gui/dgraph.mli
+/src/plugins/gui/gtk_compat.ml
+/src/plugins/gui/GSourceView.ml
+/src/plugins/gui/GSourceView.mli
diff --git a/Makefile b/Makefile
index 88062fe83bda6de971e1117a3e10f595badde2f9..6989f1c4f84879927e010c7325361e52fd407d2a 100644
--- a/Makefile
+++ b/Makefile
@@ -680,8 +680,59 @@ STARTUP_CMX=$(STARTUP_CMO:.cmo=.cmx)
WTOOLKIT= \
wutil widget wbox wfile wpane wpalette wtext wtable
+ifeq ($(strip $(GTKSOURCEVIEW)),lablgtk3.sourceview3)
+
+src/plugins/gui/GSourceView.ml: src/plugins/gui/GSourceView3.ml.in
+ $(CP) $< $@
+ $(CHMOD_RO) $@
+
+src/plugins/gui/GSourceView.mli: src/plugins/gui/GSourceView3.mli.in
+ $(CP) $< $@
+ $(CHMOD_RO) $@
+
+else
+src/plugins/gui/GSourceView.ml: src/plugins/gui/GSourceView2.ml.in
+ $(CP) $< $@
+ $(CHMOD_RO) $@
+
+src/plugins/gui/GSourceView.mli: src/plugins/gui/GSourceView2.mli.in
+ $(CP) $< $@
+ $(CHMOD_RO) $@
+
+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) $< $@
+ $(CHMOD_RO) $@
+else
+src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.2.ml
+ $(CP) $< $@
+ $(CHMOD_RO) $@
+endif
+GENERATED+=src/plugins/gui/gtk_compat.ml
+
SINGLE_GUI_CMO:= \
+ gtk_compat \
$(WTOOLKIT) \
+ $(SOURCEVIEWCOMPAT) \
+ $(DGRAPHCOMPAT) \
gui_parameters \
gtk_helper gtk_form \
source_viewer pretty_source source_manager book_manager \
@@ -734,7 +785,12 @@ PLUGIN_NAME:=Callgraph
PLUGIN_DISTRIBUTED:=yes
PLUGIN_DIR:=src/plugins/callgraph
PLUGIN_CMO:= options journalize subgraph cg services uses register
+#GTK3: no DGraph available.
+ifeq ($(HAS_GNOMECANVAS),yes)
PLUGIN_GUI_CMO:=cg_viewer
+else
+PLUGIN_GUI_CMO:=
+endif
PLUGIN_CMI:= callgraph_api
PLUGIN_INTERNAL_TEST:=yes
PLUGIN_TESTS_DIRS:=callgraph
diff --git a/configure.in b/configure.in
index bd9c9a010d412cff46fd8e5b9e979005f59cc462..147de49d195314bc4356ef16c276ce57f64e6c2f 100644
--- a/configure.in
+++ b/configure.in
@@ -741,7 +741,7 @@ plugin_require(from_analysis,callgraph)
check_plugin(gui,src/plugins/gui,[support for gui],yes)
plugin_require_external(gui,lablgtk)
-plugin_require_external(gui,gnomecanvas)
+plugin_use_external(gui,gnomecanvas)
plugin_require_external(gui,gtksourceview)
plugin_use_external(gui,dot)
@@ -921,22 +921,46 @@ new_section "configure tools and libraries used by some plug-ins"
# lablgtk2
##########
+define([ENABLE_LABLGTK3_HELP],
+ AC_HELP_STRING([--disable-lablgtk3],
+ [in case lablgtk2 and lablgtk3 are available, the default is to compile
+ against lablgtk3. Use this option to force compiling against lablgtk2]))
+
+AC_ARG_ENABLE(
+ lablgtk3,[ENABLE_LABLGTK3_HELP],
+ [ENABLE_LABLGTK3=$enableval],[ENABLE_LABLGTK3=yes])
+
REQUIRE_LABLGTK="$REQUIRE_LABLGTK$REQUIRE_GNOMECANVAS"
USE_LABLGTK="$USE_LABLGTK$USE_GNOMECANVAS"
+LABLGTK_PATH=""
+
+if test "$ENABLE_LABLGTK3" = "yes"; then
+ LABLGTK_PATH=`ocamlfind query lablgtk3 | tr -d '\\r\\n'`;
+fi
+
+if test "$LABLGTK_PATH" = ""; then
+ LABLGTK_VERSION=2
LABLGTK_PATH=`ocamlfind query lablgtk2 | tr -d '\\r\\n'`
- if test "$LABLGTK_PATH" = "" -o "$LABLGTK_PATH" -ef "$OCAMLLIB/lablgtk2" ; then
- echo "Ocamlfind -> using +lablgtk2.($LABLGTK_PATH,$OCAMLLIB/lablgtk2)"
- LABLGTK_PATH=+lablgtk2
- LABLGTKPATH_FOR_CONFIGURE=$OCAMLLIB/lablgtk2
+ if test "$LABLGTK_PATH" = "" -o \
+ "$LABLGTK_PATH" -ef "$OCAMLLIB/lablgtk2" ; then
+ echo "Ocamlfind -> using +lablgtk2.($LABLGTK_PATH,$OCAMLLIB/lablgtk2)"
+ LABLGTK_PATH=+lablgtk2
+ LABLGTKPATH_FOR_CONFIGURE=$OCAMLLIB/lablgtk2
else
- echo "Ocamlfind -> using $LABLGTK_PATH"
- LABLGTKPATH_FOR_CONFIGURE=$LABLGTK_PATH
- fi
+ echo "Ocamlfind -> using $LABLGTK_PATH"
+ LABLGTKPATH_FOR_CONFIGURE=$LABLGTK_PATH
+ fi;
+else
+ LABLGTK_VERSION=3
+ echo "ocamlfind -> using $LABLGTK_PATH"
+ LABLGTKPATH_FOR_CONFIGURE=$LABLGTK_PATH;
+fi
configure_library([GTKSOURCEVIEW],
- [$LABLGTKPATH_FOR_CONFIGURE/lablgtksourceview2.$LIB_SUFFIX],
- [lablgtksourceview2.$LIB_SUFFIX not found],
+ [$LABLGTKPATH_FOR_CONFIGURE/lablgtksourceview2.$LIB_SUFFIX,
+ $LABLGTKPATH_FOR_CONFIGURE/lablgtksourceview3.$LIB_SUFFIX],
+ [lablgtksourceview not found],
no)
configure_library([GNOMECANVAS],
@@ -991,6 +1015,7 @@ AC_SUBST(HAS_YOJSON)
AC_SUBST(HAS_APRON)
AC_SUBST(HAS_MPFR)
AC_SUBST(HAS_LANDMARKS)
+AC_SUBST(LABLGTK_VERSION)
AC_SUBST(OCAMLBEST)
AC_SUBST(OCAMLVERSION)
AC_SUBST(OCAMLLIB)
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 53fa80a1a72a5c701eb535f708636072c3040b56..0a279499223744d29686aa8da1ff084dab09e751 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -755,6 +755,10 @@ src/plugins/from/from_register_gui.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/from/from_register_gui.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/from/functionwise.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/from/functionwise.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/GSourceView2.ml.in: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/GSourceView2.mli.in: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/GSourceView3.ml.in: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/GSourceView3.mli.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/analyses_manager.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/analyses_manager.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/book_manager.ml: CEA_LGPL_OR_PROPRIETARY
@@ -763,10 +767,15 @@ src/plugins/gui/debug_manager.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/debug_manager.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/design.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/design.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/dgraph.ml.in: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/dgraph.mli.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/file_manager.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/file_manager.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/filetree.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/filetree.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/gtk_compat.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/gtk_compat.2.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/gui/gtk_compat.3.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/gtk_form.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/gtk_form.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/gui/gtk_helper.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index 993b677842a1f90c021bf18d911c88be1b97448a..3b3bb7b71ae5bc96d89a10bd4025fd59d0ec23df 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -102,10 +102,13 @@ DEVELOPMENT ?=@DEVELOPMENT@
HAS_LABLGTK ?=@HAS_LABLGTK@
HAS_LABLGTK_CUSTOM_MODEL ?=@HAS_LABLGTK@
LABLGTK_PATH ?=@LABLGTK_PATH@
-
+LABLGTK ?= lablgtk@LABLGTK_VERSION@
# lablgtksourceview
HAS_GTKSOURCEVIEW ?=@HAS_GTKSOURCEVIEW@
+GTKSOURCEVIEW:=\
+ $(patsubst lablgtk%,$(LABLGTK).%,$(basename $(notdir @GTKSOURCEVIEW@)))
+
# lablgnomecanvas
HAS_GNOMECANVAS ?=@HAS_GNOMECANVAS@
@@ -190,7 +193,10 @@ LIBRARY_NAMES += yojson
endif
ifneq ($(ENABLE_GUI),no)
-LIBRARY_NAMES_GUI = lablgtk2 lablgtk2.gnomecanvas lablgtk2.sourceview2
+ LIBRARY_NAMES_GUI = $(LABLGTK) $(GTKSOURCEVIEW)
+ ifeq ($(HAS_GNOMECANVAS),yes)
+ LIBRARY_NAMES_GUI+=lablgtk2.gnomecanvas
+ endif
else
LIBRARY_NAMES_GUI =
endif
diff --git a/src/plugins/gui/GSourceView2.ml.in b/src/plugins/gui/GSourceView2.ml.in
new file mode 100644
index 0000000000000000000000000000000000000000..89f79dcaf149884732b46b7764800e870cba4223
--- /dev/null
+++ b/src/plugins/gui/GSourceView2.ml.in
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** compatibility layer between gtksourceview 2 and 3. *)
+include GSourceView2
+
+let make_marker_attributes
+ ~(source:source_view)
+ ~(category:string)
+ ~(priority: int)
+ ?(background: Gdk.color option)
+ ?(pixbuf:GdkPixbuf.pixbuf option)
+ ?(icon_name:string option)
+ () =
+ ignore icon_name; (* not in lablgtk2. *)
+ source#set_mark_category_priority ~category priority;
+ source#set_mark_category_pixbuf ~category pixbuf;
+ source#set_mark_category_background ~category background
diff --git a/src/plugins/gui/GSourceView2.mli.in b/src/plugins/gui/GSourceView2.mli.in
new file mode 100644
index 0000000000000000000000000000000000000000..161de3e384c7636ed149aae3a84316e04f9ce16b
--- /dev/null
+++ b/src/plugins/gui/GSourceView2.mli.in
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* compatibility between gtksourceview 2 and 3. *)
+include module type of GSourceView2
+
+val make_marker_attributes:
+ source:source_view ->
+ category:string ->
+ priority: int ->
+ ?background: Gdk.color ->
+ ?pixbuf:GdkPixbuf.pixbuf ->
+ ?icon_name:string ->
+ unit ->
+ unit
diff --git a/src/plugins/gui/GSourceView3.ml.in b/src/plugins/gui/GSourceView3.ml.in
new file mode 100644
index 0000000000000000000000000000000000000000..ddce6f7a849c3377fcfba1626158562f3c548933
--- /dev/null
+++ b/src/plugins/gui/GSourceView3.ml.in
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** compatibility layer between gtksourceview 2 and 3. *)
+include GSourceView3
+
+let make_marker_attributes
+ ~(source:source_view)
+ ~(category:string)
+ ~(priority: int)
+ ?(background: Gdk.rgba option)
+ ?(pixbuf:GdkPixbuf.pixbuf option)
+ ?(icon_name:string option)
+ () =
+ let my_attributes = GSourceView3.source_mark_attributes () in
+ Extlib.may my_attributes#set_background background;
+ Extlib.may my_attributes#set_pixbuf pixbuf;
+ Extlib.may my_attributes#set_icon_name icon_name;
+ source#set_mark_attributes ~category my_attributes priority
diff --git a/src/plugins/gui/GSourceView3.mli.in b/src/plugins/gui/GSourceView3.mli.in
new file mode 100644
index 0000000000000000000000000000000000000000..4433f0ee169ac7e4f93e6ff183c3aaa2d0884f06
--- /dev/null
+++ b/src/plugins/gui/GSourceView3.mli.in
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* compatibility between gtksourceview 2 and 3. *)
+include module type of GSourceView3
+
+val make_marker_attributes:
+ source:source_view ->
+ category:string ->
+ priority: int ->
+ ?background: Gdk.rgba ->
+ ?pixbuf:GdkPixbuf.pixbuf ->
+ ?icon_name:string ->
+ unit ->
+ unit
diff --git a/src/plugins/gui/book_manager.ml b/src/plugins/gui/book_manager.ml
index 6b8d8785350055d8c59a7c7ea77d5130ef90e1d6..0be6a2e576e8a80b2485019732e3d5e8d0372653 100644
--- a/src/plugins/gui/book_manager.ml
+++ b/src/plugins/gui/book_manager.ml
@@ -24,7 +24,7 @@ let dkey = Gui_parameters.register_category "book_manager"
module Q = Qstack.Make
(struct
- type t = GSourceView2.source_view
+ type t = GSourceView.source_view
let equal x y = x == y
end)
@@ -112,7 +112,7 @@ let delete_all_views (t:t) =
Q.iter (fun _ -> t.notebook#remove_page 0) t.views;
Q.clear t.views
-let append_view (t:t) (v:GSourceView2.source_view) =
+let append_view (t:t) (v:GSourceView.source_view) =
let nb = t.notebook in
let next = Q.length t.views in
let text = Printf.sprintf "Page %d" next in
diff --git a/src/plugins/gui/book_manager.mli b/src/plugins/gui/book_manager.mli
index 3d96b5f103caad40097aaef574317023dd4586ef..c3b8df28b766030070e09c2d6a8832f804b39b2b 100644
--- a/src/plugins/gui/book_manager.mli
+++ b/src/plugins/gui/book_manager.mli
@@ -34,9 +34,9 @@ val make:
val get_notebook: t -> GPack.notebook
-val append_source_tab : t -> string -> GSourceView2.source_view
+val append_source_tab : t -> string -> GSourceView.source_view
-val prepend_source_tab : t -> string -> GSourceView2.source_view
+val prepend_source_tab : t -> string -> GSourceView.source_view
val get_nth_page: t -> int -> GObj.widget
@@ -46,7 +46,7 @@ val last_page: t -> int
val set_current_view: t -> int -> unit
-val get_current_view: t -> GSourceView2.source_view
+val get_current_view: t -> GSourceView.source_view
val get_current_index: t -> int
@@ -56,9 +56,9 @@ val delete_view: t -> int -> unit
val delete_all_views: t -> unit
-val append_view: t -> GSourceView2.source_view -> unit
+val append_view: t -> GSourceView.source_view -> unit
-val get_nth_view: t -> int -> GSourceView2.source_view
+val get_nth_view: t -> int -> GSourceView.source_view
val enable_popup : t -> bool -> unit
diff --git a/src/plugins/gui/debug_manager.ml b/src/plugins/gui/debug_manager.ml
index 4d7e45a1d505eca845707c743f67b47296ad77c9..6f8def06cba235523e513618e8921f1f6ab4686b 100644
--- a/src/plugins/gui/debug_manager.ml
+++ b/src/plugins/gui/debug_manager.ml
@@ -49,9 +49,7 @@ let graph_window main_window title mk_view =
let height = int_of_float (float main_window#default_height *. 3. /. 4.) in
let width = int_of_float (float main_window#default_width *. 3. /. 4.) in
let window =
- GWindow.window
- ~width ~height ~title ~allow_shrink:true ~allow_grow:true
- ~position:`CENTER ()
+ GWindow.window ~width ~height ~title ~resizable:true ~position:`CENTER ()
in
let view = mk_view ~packing:window#add () in
window#show ();
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index d695a38cb3a02e8a70074293c30ec6e5127737e6..6fb4e4657dc6ce63cd257d832094b3e0fc1c48d3 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -34,7 +34,7 @@ let use_external_viewer = false
class type reactive_buffer = object
inherit error_manager
- method buffer : GSourceView2.source_buffer
+ method buffer : GSourceView.source_buffer
method locs : Pretty_source.Locs.state
method rehighlight: unit
method redisplay: unit
@@ -61,7 +61,7 @@ class type main_window_extension_points = object
(** Pretty print a message in the [annot_window]. *)
method launcher : unit -> unit
- method source_viewer : GSourceView2.source_view
+ method source_viewer : GSourceView.source_view
method source_viewer_scroll : GBin.scrolled_window
method display_globals : global list -> unit
method register_source_selector :
@@ -657,20 +657,19 @@ struct
let fold_category = "fold"
let unfold_category = "unfold"
- let declare_markers (source:GSourceView2.source_view) =
- source#set_mark_category_pixbuf
- ~category:fold_category (Some Gtk_helper.Icon.(get Fold));
- source#set_mark_category_pixbuf
- ~category:unfold_category (Some Gtk_helper.Icon.(get Unfold));
- (* Sets a high prioriy so that the icon for folding and unfolding are
- printed on top of the status bullets. *)
- source#set_mark_category_priority ~category:fold_category 2;
- source#set_mark_category_priority ~category:unfold_category 2;
+(*GTK3 does not exist anymore in gsourceview3. *)
+ let declare_markers (source:GSourceView.source_view) =
+ GSourceView.make_marker_attributes
+ ~source ~category:fold_category ~priority:2
+ ~pixbuf:(Gtk_helper.Icon.(get Fold)) ();
+ GSourceView.make_marker_attributes
+ ~source ~category:unfold_category ~priority:2
+ ~pixbuf:(Gtk_helper.Icon.(get Unfold)) ();
List.iter
(fun v ->
- source#set_mark_category_pixbuf
- ~category:(category v)
- (Some (Gtk_helper.Icon.get (Gtk_helper.Icon.Feedback v))))
+ GSourceView.make_marker_attributes
+ ~source ~category:(category v) ~priority:1
+ ~pixbuf:(Gtk_helper.Icon.get (Gtk_helper.Icon.Feedback v)) ())
[ F.Never_tried;
F.Considered_valid;
F.Valid;
@@ -695,19 +694,20 @@ struct
Hashtbl.clear tooltip_marks;
Hashtbl.clear call_sites
- let mark (source:GSourceView2.source_buffer) ?call_site ~offset validity =
+ let mark (source:GSourceView.source_buffer) ?call_site ~offset validity =
let iter = source#get_iter_at_char offset in
+ let mark = iter#set_line_offset 0 in
let category = category validity in
- source#remove_source_marks iter iter () ;
- ignore (source#create_source_mark ~category iter) ;
+ source#remove_source_marks mark mark () ;
+ ignore (source#create_source_mark ~category mark) ;
Hashtbl.replace tooltip_marks iter#line (long_category validity);
match call_site with
| None -> ()
| Some stmt ->
Hashtbl.replace call_sites iter#line stmt;
if Pretty_source.are_preconds_unfolded stmt
- then ignore (source#create_source_mark ~category:fold_category iter)
- else ignore (source#create_source_mark ~category:unfold_category iter)
+ then ignore (source#create_source_mark ~category:fold_category mark)
+ else ignore (source#create_source_mark ~category:unfold_category mark)
end
@@ -846,8 +846,7 @@ class main_window () : main_window_extension_points =
~width
~height
~position:`CENTER
- ~allow_shrink:true
- ~allow_grow:true
+ ~resizable:true
~show:false
()
in
@@ -865,9 +864,7 @@ class main_window () : main_window_extension_points =
in
(* status bar (at bottom) *)
(* toplevel_vbox->bottom_hbox-> *statusbar *)
- let statusbar =
- GMisc.statusbar ~has_resize_grip:false ~packing:bottom_hbox#add ()
- in
+ let statusbar = GMisc.statusbar ~packing:bottom_hbox#add () in
let status_context = statusbar#new_context "messages" in
(* progress bar (at bottom) *)
@@ -1187,6 +1184,10 @@ class main_window () : main_window_extension_points =
let show o =
history (fun () -> History.push (History.Localizable loc));
let iter = self#source_viewer#buffer#get_iter (`OFFSET o) in
+ Gui_parameters.debug
+ ~dkey:dkey_scroll "scrolling in current view at iter %d,%d"
+ iter#line iter#line_offset
+ ;
ignore (self#source_viewer#backward_display_line_start iter);
self#source_viewer#buffer#place_cursor iter;
ignore (self#source_viewer#scroll_to_mark
@@ -1367,7 +1368,7 @@ class main_window () : main_window_extension_points =
to be found (e.g. Ctrl+F). Otherwise, uses the last searched
text (e.g. F3). *)
method private focused_find_text use_dialog =
- let find_text_in_viewer ~where (viewer : [`GTextViewer of GText.view |`GSourceViewer of GSourceView2.source_view]) text =
+ let find_text_in_viewer ~where (viewer : [`GTextViewer of GText.view |`GSourceViewer of GSourceView.source_view]) text =
let buffer, scroll_to_iter =
match viewer with
| `GTextViewer v -> v#buffer,v#scroll_to_iter
@@ -1497,11 +1498,22 @@ class main_window () : main_window_extension_points =
let abs_x = int_of_float (GdkEvent.Button.x_root ev) in
(* This function returns the absolute position of the top window,
or the relative position of an intern widget. *)
+ let rec get_rel_from_main acc win =
+ let x = fst (Gdk.Window.get_position win) in
+ let acc = acc + x in
+ let win = Gdk.Window.get_parent win in
+ if Gobject.get_oid win =
+ Gobject.get_oid main_window#misc#window
+ then acc
+ else get_rel_from_main acc win
+ in
let get_x obj = fst (Gdk.Window.get_position obj#misc#window) in
(* Absolute position of the main window on the screen. *)
let window_abs_x = get_x main_window in
(* Relative position of the source_viewer in the main windows. *)
- let viewer_rel_x = get_x source_viewer in
+ let viewer_rel_x =
+ get_rel_from_main 0 source_viewer#misc#window
+ in
(* Width of the bullet column in the source viewer. *)
if abs_x - (window_abs_x + viewer_rel_x) < 20 then
begin
@@ -1513,15 +1525,76 @@ class main_window () : main_window_extension_points =
let line = iterpos#line in
try
let stmt = Hashtbl.find Feedback.call_sites line in
- let kf = Kernel_function.find_englobing_kf stmt in
Pretty_source.fold_preconds_at_callsite stmt;
- self#reactive_buffer#redisplay;
- self#scroll (PStmt (kf, stmt))
- with Not_found -> ()
+ self#reset ();
+ (* give some time for the sourceview to recompute
+ its height, otherwise scrolling is broken. *)
+ let has_stabilized = ref false in
+ (* According to the blog post here
+ https://picheta.me/articles/2013/08/gtk-plus--a-method-to-guarantee-scrolling.html
+ the best way to check whether we have correctly scrolled
+ is to retrieve the rectangle corresponding to the mark,
+ the rectangle effectively displayed, and see whether
+ the former is included in the latter.
+ *)
+ let check () =
+ (* not entirely accurate because of
+ the (un)fold action, but should do the trick.
+ We will do the real scroll after stabilization
+ anyway.
+ *)
+ let iter =
+ source_viewer#buffer#get_iter (`LINE line)
+ in
+ let my_rect = source_viewer#get_iter_location iter in
+ let visible_rect = source_viewer#visible_rect in
+ (* in Gdk, x,y represents the top left corner of the
+ rectangle. We just check whether the beginning of the
+ selection is visible (we only have one line of text
+ anyway). *)
+ let res =
+ Gdk.Rectangle.(
+ y my_rect >= y visible_rect &&
+ y my_rect <= y visible_rect + height visible_rect
+ )
+ in
+ Gdk.Rectangle.(Gui_parameters.debug ~dkey:dkey_scroll
+ "my rect is %d (+%d) %d (+%d)@\n\
+ vis rect is %d (+%d) %d (+%d)@\n\
+ my rect is visible: %B@."
+ (x my_rect) (width my_rect) (y my_rect) (height my_rect)
+ (x visible_rect) (width visible_rect) (y visible_rect)
+ (height visible_rect) res);
+ has_stabilized := res;
+ (* when added as an idle procedure below, check will
+ be removed whenever it returns false. *)
+ not res
+ in
+ (* in case we were lucky and have stabilized directly. *)
+ ignore (check());
+ let proc = Glib.Idle.add check in
+ (* in case we are unlucky, stop waiting after
+ 0.5 second and hope for the best. *)
+ let alarm =
+ Glib.Timeout.add
+ ~ms:500
+ ~callback:
+ (fun () ->
+ has_stabilized := true;
+ Glib.Idle.remove proc;
+ false)
+ in
+ while (not !has_stabilized) do
+ (* do one main loop step so that buffer gets
+ a chance to recompute its height. *)
+ ignore (Glib.Main.iteration false)
+ done;
+ Glib.Timeout.remove alarm;
+ self#view_stmt stmt;
+ with Not_found -> ()
end;
false)
in
-
let extra_accel_group = GtkData.AccelGroup.create () in
GtkData.AccelGroup.connect extra_accel_group
~key:GdkKeysyms._F
diff --git a/src/plugins/gui/design.mli b/src/plugins/gui/design.mli
index 7c6da50093d8633d871bd005c4a3ad0c6612c5bf..2d26d4de1d3615d4266d2e692ec478fe3b9be6f8 100644
--- a/src/plugins/gui/design.mli
+++ b/src/plugins/gui/design.mli
@@ -30,7 +30,7 @@ open Cil_types
@since Beryllium-20090901 *)
class type reactive_buffer = object
inherit Gtk_helper.error_manager
- method buffer : GSourceView2.source_buffer
+ method buffer : GSourceView.source_buffer
method locs : Pretty_source.Locs.state
method rehighlight : unit
method redisplay : unit
@@ -122,7 +122,7 @@ class type main_window_extension_points = object
(** {4 Source viewers} *)
- method source_viewer : GSourceView2.source_view
+ method source_viewer : GSourceView.source_view
(** The [GText.view] showing the AST. *)
method source_viewer_scroll : GBin.scrolled_window
@@ -172,7 +172,7 @@ class type main_window_extension_points = object
top of the other.
@modify Aluminium-20160501: receives a {!reactive_buffer} instead
- of a {!GSourceView2.source_buffer} *)
+ of a {!GSourceView.source_buffer} *)
method register_panel :
(main_window_extension_points->(string*GObj.widget*(unit-> unit) option))
@@ -263,14 +263,14 @@ val reactive_buffer : main_window_extension_points ->
module Feedback :
sig
- val declare_markers: GSourceView2.source_view -> unit
+ val declare_markers: GSourceView.source_view -> unit
(** Declares the icons used for the property status bullets, as marks in
the left-margin of the source buffer.
These icons depend on the GUI theme, and must be reset when the
theme is changed.
@since Chlorine-20180501 *)
- val mark : GSourceView2.source_buffer
+ val mark : GSourceView.source_buffer
-> ?call_site:stmt
-> offset:int
-> Property_status.Feedback.t -> unit
diff --git a/src/plugins/gui/dgraph.ml.in b/src/plugins/gui/dgraph.ml.in
new file mode 100644
index 0000000000000000000000000000000000000000..5271e01436fc8a5fd4dd03236edc3aa5a4c6cae8
--- /dev/null
+++ b/src/plugins/gui/dgraph.ml.in
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* 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 = 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
diff --git a/src/plugins/gui/dgraph.mli.in b/src/plugins/gui/dgraph.mli.in
new file mode 100644
index 0000000000000000000000000000000000000000..902aed1c043628d30a1fa31a3e68aef61329528a
--- /dev/null
+++ b/src/plugins/gui/dgraph.mli.in
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* 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/filetree.ml b/src/plugins/gui/filetree.ml
index b835d12d195d52148fc8f004cb4e5b1bb246d5b2..7b83952df6744e60a0defd40b32810401c0b6060 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -630,7 +630,7 @@ let make (tree_view:GTree.view) =
let column = GTree.view_column ~renderer:(renderer,[]) () in
ignore (tree_view#append_column column);
let label = GMisc.label ~text:title () in
- (GData.tooltips ())#set_tip ~text:tooltip label#coerce;
+ Gtk_helper.do_tooltip ~tooltip label;
column#set_widget (Some label#coerce);
column#set_alignment 0.5;
column#set_reorderable true;
diff --git a/src/plugins/gui/gtk_compat.2.ml b/src/plugins/gui/gtk_compat.2.ml
new file mode 100644
index 0000000000000000000000000000000000000000..dd739106fd66eacdf0f14c072574eb6d1db5b416
--- /dev/null
+++ b/src/plugins/gui/gtk_compat.2.ml
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+let get_toolbar_index (toolbar:GButton.toolbar) (item:GButton.tool_item) =
+ toolbar#get_item_index item
diff --git a/src/plugins/gui/gtk_compat.3.ml b/src/plugins/gui/gtk_compat.3.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e790d9ea307360068a28367fb7e46e65ca253d34
--- /dev/null
+++ b/src/plugins/gui/gtk_compat.3.ml
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+let get_toolbar_index toolbar item = toolbar#get_item_index item#as_tool_item
diff --git a/src/plugins/gui/gtk_compat.mli b/src/plugins/gui/gtk_compat.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f7d4afd6d165564609079d2db37ab85094a98ad5
--- /dev/null
+++ b/src/plugins/gui/gtk_compat.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val get_toolbar_index: GButton.toolbar -> GButton.tool_item -> int
diff --git a/src/plugins/gui/gtk_form.ml b/src/plugins/gui/gtk_form.ml
index 2054b86d0f53785a83780613f6f0dca96062ebeb..0d55967df72f5bc441f6b3f68ff32a19e63b6ea8 100644
--- a/src/plugins/gui/gtk_form.ml
+++ b/src/plugins/gui/gtk_form.ml
@@ -40,12 +40,6 @@ type 'a field =
?tooltip:string -> packing:(GObj.widget -> unit) ->
(unit -> 'a) -> ('a -> unit) -> demon -> unit
-let mk_tooltip ?tooltip obj = match tooltip with
- | None -> ()
- | Some text ->
- let tooltip = GData.tooltips () in
- tooltip#set_tip ~text obj#coerce
-
(* ------------------------------------------------------------------------ *)
(* --- Check Button --- *)
(* ------------------------------------------------------------------------ *)
@@ -54,7 +48,7 @@ let check ?label ?tooltip ~packing get set demon =
let button =
GButton.check_button ?label ~packing ~active:(get ()) ()
in
- mk_tooltip ?tooltip button ;
+ Gtk_helper.do_tooltip ?tooltip button ;
ignore (button#connect#toggled ~callback:(fun () -> set button#active));
register demon (fun () -> button#set_active (get()))
@@ -88,7 +82,7 @@ let menu entries ?width ?tooltip ~packing get set demon =
with Not_found -> ()
in
ignore (combo_box#connect#changed callback) ;
- mk_tooltip ?tooltip combo_box ;
+ Gtk_helper.do_tooltip ?tooltip combo_box ;
register demon update
(* ------------------------------------------------------------------------ *)
@@ -105,7 +99,7 @@ let spinner ?(lower=0) ?(upper=max_int) ?width ?tooltip ~packing get set demon =
if a<>b then set a in
let update () = spin#adjustment#set_value (float (get ())) in
ignore (spin#connect#value_changed ~callback) ;
- mk_tooltip ?tooltip spin ;
+ Gtk_helper.do_tooltip ?tooltip spin ;
register demon update
(* ------------------------------------------------------------------------ *)
@@ -137,5 +131,5 @@ let label ~text ~packing () =
let button ~label ?tooltip ~callback ~packing () =
let b = GButton.button ~label ~packing () in
- mk_tooltip ?tooltip b ;
+ Gtk_helper.do_tooltip ?tooltip b ;
ignore (b#connect#clicked ~callback)
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 0846a32080233072d06895460030f95c9ae73788..bbc2ab55ba43512f32214b91c1e11cd3093bca41 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -359,9 +359,7 @@ type 'a chooser =
let do_tooltip ?tooltip obj = match tooltip with
| None -> ()
- | Some text ->
- let tooltip = GData.tooltips () in
- tooltip#set_tip ~text obj#coerce
+ | Some text -> obj#coerce#misc#set_tooltip_text text
let on_bool ?tooltip ?use_markup (container:GPack.box) label get set =
let result = ref (get ()) in
@@ -550,10 +548,13 @@ let trace_event (w:GObj.event_ops) =
| `DROP_FINISHED -> "drop-finish"
| `CLIENT_EVENT -> "client-event"
| `VISIBILITY_NOTIFY -> "visibility-notify"
- | `NO_EXPOSE-> "no-expose"
+ (*GTK3 Event does not exist anymore *)
+ (* | `NO_EXPOSE-> "no-expose" *)
| `SCROLL -> "scroll"
| `WINDOW_STATE -> "window-state"
| `SETTING -> "setting"
+ (*GTK3: leave room for more events. *)
+ | _ -> "unknown-gtk3-event"
in
ignore (w#connect#any
~callback:(fun e ->
@@ -959,6 +960,45 @@ let source_files_chooser (main_ui: source_files_chooser_host) defaults f =
dialog#show ();
()
+let default_dir = ref ""
+
+let select_file ?title ?(dir=default_dir) ?(filename="") () =
+ let filename =
+ if Filename.is_relative filename then
+ if !dir <> "" then !dir ^ "/" ^ filename
+ else ""
+ else begin
+ dir:= Filename.dirname filename;
+ filename
+ end
+ in
+ let dialog: GWindow.Buttons.file_selection GWindow.file_chooser_dialog =
+ GWindow.file_chooser_dialog
+ ~action:`OPEN
+ ?title
+ ~modal:true
+ ()
+ in
+ ignore (dialog#set_filename filename);
+ let result = ref None in
+ let action r =
+ (match r with
+ | `OK ->
+ let file = dialog#filename in
+ (match file with
+ | None -> ()
+ | Some file ->
+ dir := Filename.dirname file;
+ result := Some file)
+ | _ -> ());
+ dialog#destroy ()
+ in
+ dialog#add_select_button "Open" `OK;
+ dialog#add_button "Cancel" `CANCEL;
+ dialog#show ();
+ action (dialog#run ());
+ !result
+
let spawn_command ?(timeout=0) ?stdout ?stderr s args f =
let check_result = Command.command_async s ?stdout ?stderr args in
let has_timeout = timeout > 0 in
@@ -984,8 +1024,8 @@ let graph_window ~parent ~title make_view =
let width = int_of_float (float parent#default_width *. 3. /. 4.) in
let graph_window =
GWindow.window
- ~width ~height ~title ~allow_shrink:true ~allow_grow:true
- ~position:`CENTER () in
+ ~width ~height ~title ~resizable:true ~position:`CENTER ()
+ in
let view = make_view ~packing:graph_window#add () in
graph_window#show();
view#adapt_zoom();
@@ -1017,6 +1057,16 @@ let graph_window_through_dot ~parent ~title dot_formatter =
(Printexc.to_string exn)
;;
+let image_menu_item ~(image:GObj.widget) ~text ~packing =
+ let mi = GMenu.menu_item () in
+ let box =
+ GPack.hbox ~spacing:2 ~border_width:0 ~packing:mi#add ()
+ in
+ box#add image;
+ box#add (GMisc.label ~justify:`LEFT ~xalign:0. ~xpad:0 ~text ())#coerce;
+ packing mi;
+ mi
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/gui/gtk_helper.mli b/src/plugins/gui/gtk_helper.mli
index 679ebc2165cc9311ec086f817d689bb3248abbdc..d054ff6847e8f25eb6c347b95a391d984144140d 100644
--- a/src/plugins/gui/gtk_helper.mli
+++ b/src/plugins/gui/gtk_helper.mli
@@ -162,11 +162,11 @@ val make_tag :
create_tag : ?name:string -> GText.tag_property list -> GText.tag ; .. >
-> name:string -> GText.tag_property list -> GText.tag
-val apply_tag : GSourceView2.source_buffer -> GText.tag -> int -> int -> unit
-val remove_tag : GSourceView2.source_buffer -> GText.tag -> int -> int -> unit
-val cleanup_tag : GSourceView2.source_buffer -> GText.tag -> unit
+val apply_tag : GSourceView.source_buffer -> GText.tag -> int -> int -> unit
+val remove_tag : GSourceView.source_buffer -> GText.tag -> int -> int -> unit
+val cleanup_tag : GSourceView.source_buffer -> GText.tag -> unit
-val cleanup_all_tags : GSourceView2.source_buffer -> unit
+val cleanup_all_tags : GSourceView.source_buffer -> unit
(* ************************************************************************** *)
(** {2 Channels} *)
@@ -321,6 +321,15 @@ val source_files_chooser:
(string list -> unit) ->
unit
+(** Launches a standard gtk file chooser window and returns the name
+ of the selected file. Replaces GToolbox.select_file that has not been
+ ported to lablgtk3.
+
+ @since Frama-C+dev
+*)
+val select_file:
+ ?title:string -> ?dir:(string ref)-> ?filename:string -> unit -> string option
+
(* ************************************************************************** *)
(** {2 Miscellaneous} *)
(* ************************************************************************** *)
@@ -432,6 +441,16 @@ val graph_window_through_dot:
(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
+*)
+val image_menu_item:
+ image:GObj.widget ->
+ text: string ->
+ packing: (GMenu.menu_item -> unit) ->
+ GMenu.menu_item
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/gui/launcher.ml b/src/plugins/gui/launcher.ml
index 24761d0f03f493a6f77abbf0c2ead3deb7f63bd5..fd8db91cf27e7d23cb4a1da1633d4bf50f488213 100644
--- a/src/plugins/gui/launcher.ml
+++ b/src/plugins/gui/launcher.ml
@@ -253,11 +253,10 @@ let show ?height ?width ~(host:basic_main) () =
~title:"Launching analysis"
~modal:true
~position:`CENTER_ON_PARENT
- ~allow_shrink:true
+ ~resizable:true
?width
?height
~parent:host#main_window
- ~allow_grow:true
()
in
ignore (dialog#misc#connect#size_allocate
diff --git a/src/plugins/gui/menu_manager.ml b/src/plugins/gui/menu_manager.ml
index 0388411e620570cb58e3f13895611f70084c5a02..7cf32bfc19a141ae07f614c417976d0f0063a715 100644
--- a/src/plugins/gui/menu_manager.ml
+++ b/src/plugins/gui/menu_manager.ml
@@ -165,7 +165,10 @@ class menu_manager ?packing ~host:(_:Gtk_helper.host) =
By default, add all the others just before this very first group. *)
ref (match pos, first_tool_separator with
| None, None -> 0
- | None, Some sep -> max 0 (toolbar#get_item_index sep)
+ | None, Some sep ->
+ max
+ 0
+ (Gtk_compat.get_toolbar_index toolbar (sep:>GButton.tool_item))
| Some p, _ -> p)
in
let toolbar_packing w =
@@ -213,7 +216,7 @@ class menu_manager ?packing ~host:(_:Gtk_helper.host) =
(fun () -> b#set_active (active ())) :: set_active_states;
BToggle b
in
- (bt_type_as_skel b)#set_tooltip (GData.tooltips ()) tooltip "";
+ (bt_type_as_skel b)#misc#set_tooltip_text tooltip;
toolbar_buttons <- (b, sensitive) :: toolbar_buttons;
b
in
@@ -249,12 +252,10 @@ class menu_manager ?packing ~host:(_:Gtk_helper.host) =
ignore (mi#connect#activate callback);
MStandard mi
| Some stock, Unit_callback callback ->
- let image = GMisc.image ~stock () in
- let mi =
- (GMenu.image_menu_item
- ~image ~packing:!!menubar_packing ~label ()
- :> GMenu.menu_item)
- in
+ let image = (GMisc.image ~stock ~xalign:0. () :> GObj.widget) in
+ let text = label in
+ let packing = !!menubar_packing in
+ let mi = Gtk_helper.image_menu_item ~image ~text ~packing in
ignore (mi#connect#activate callback);
MStandard mi
| _, Bool_callback (callback, active) ->
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index 9bd7e7586f61a621f3bf1316e0e1b99fa52dc7f4..2a4133253e935f9b747b77825ad9828c2003e0cb 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -746,7 +746,7 @@ let buffer_formatter state source =
gtk_fmt
let display_source globals
- (source:GSourceView2.source_buffer) ~(host:Gtk_helper.host)
+ (source:GSourceView.source_buffer) ~(host:Gtk_helper.host)
~highlighter ~selector state =
Locs.clear state;
host#protect
diff --git a/src/plugins/gui/pretty_source.mli b/src/plugins/gui/pretty_source.mli
index 2f7473458f9abf6e00020fd60e7211b448915652..c6ee23a61a8bd6cc8a044fb0956dd6829d29f7f4 100644
--- a/src/plugins/gui/pretty_source.mli
+++ b/src/plugins/gui/pretty_source.mli
@@ -59,7 +59,7 @@ val are_preconds_unfolded: stmt -> bool
val display_source :
global list ->
- GSourceView2.source_buffer ->
+ GSourceView.source_buffer ->
host:Gtk_helper.host ->
highlighter:(localizable -> start:int -> stop:int -> unit) ->
selector:(button:int -> localizable -> unit) ->
diff --git a/src/plugins/gui/project_manager.ml b/src/plugins/gui/project_manager.ml
index abea1ed48444ccfd1823969b6098c29cc284846c..457cc3765bcb93447db6797d62d79618fd20eb17 100644
--- a/src/plugins/gui/project_manager.ml
+++ b/src/plugins/gui/project_manager.ml
@@ -218,10 +218,9 @@ and mk_project_entry window menu ?group p =
let box = GPack.hbox ~packing:p_item#add () in
ignore (GMisc.label ~text:pname ~packing:box#pack ());
let buttons_box = GPack.hbox ~packing:(box#pack ~from:`END) () in
- let tooltips = GData.tooltips () in
let add_action stock text callback =
let item = GButton.button ~packing:buttons_box#pack () in
- tooltips#set_tip item#coerce ~text;
+ Gtk_helper.do_tooltip ~tooltip:text item;
item#set_relief `NONE;
let image = GMisc.image ~stock () in
item#set_image image#coerce;
diff --git a/src/plugins/gui/source_manager.ml b/src/plugins/gui/source_manager.ml
index 08704a4f1b475140291a96d98993b39f574d75be..914bdeb731a245f8d316bd66d74ca7bc9273e10e 100644
--- a/src/plugins/gui/source_manager.ml
+++ b/src/plugins/gui/source_manager.ml
@@ -25,7 +25,7 @@ type tab = {
tab_file : Datatype.Filepath.t ;
tab_page : int ;
tab_select : line:int -> unit ;
- tab_source_view : GSourceView2.source_view;
+ tab_source_view : GSourceView.source_view;
}
type t = {
diff --git a/src/plugins/gui/source_manager.mli b/src/plugins/gui/source_manager.mli
index 013cc6d35c6dfa65d11594e979a8b0b53c6cb8e4..2f872034c48214fb3d0df70148bc126da63cc0bd 100644
--- a/src/plugins/gui/source_manager.mli
+++ b/src/plugins/gui/source_manager.mli
@@ -45,7 +45,7 @@ val load_file:
val select_file: t -> Datatype.Filepath.t -> unit (** Selection by page filename *)
val select_name: t -> string -> unit (** Selection by page title *)
-val get_current_source_view : t -> GSourceView2.source_view
+val get_current_source_view : t -> GSourceView.source_view
(** Returns the source viewer for the currently displayed tab *)
val clear : t -> unit
diff --git a/src/plugins/gui/source_viewer.ml b/src/plugins/gui/source_viewer.ml
index 0b7d27c8cd10cb5cd251e864fb868df05fe3327d..dbe8955845aecf390a8a0d2a229ecabd1227ee38 100644
--- a/src/plugins/gui/source_viewer.ml
+++ b/src/plugins/gui/source_viewer.ml
@@ -23,9 +23,9 @@
(* Build a read only text view for C source code. *)
-let set_language_to_C (buffer:GSourceView2.source_buffer) =
+let set_language_to_C (buffer:GSourceView.source_buffer) =
let original_source_language_manager =
- GSourceView2.source_language_manager ~default:true
+ GSourceView.source_language_manager ~default:true
in
let original_lang =
original_source_language_manager#guess_language
@@ -44,7 +44,7 @@ let make ?name ~packing () =
Utf8_logic.forall Utf8_logic.exists Utf8_logic.eq Utf8_logic.neq) ;
*)
let original_source_window =
- GSourceView2.source_view
+ GSourceView.source_view
~show_line_numbers:true
~editable:false
~packing
@@ -69,6 +69,6 @@ let make ?name ~packing () =
let buffer () =
- let original_source_buffer = GSourceView2.source_buffer () in
+ let original_source_buffer = GSourceView.source_buffer () in
set_language_to_C original_source_buffer;
original_source_buffer
diff --git a/src/plugins/gui/source_viewer.mli b/src/plugins/gui/source_viewer.mli
index 7a3ef5e6ba0566ebff87867aa6539e429f22d927..ab0d8cdc1d379bedbb709c1289e43dc87a153142 100644
--- a/src/plugins/gui/source_viewer.mli
+++ b/src/plugins/gui/source_viewer.mli
@@ -24,8 +24,8 @@
That is the buffer where Frama-C puts its pretty-printed AST. *)
val make : ?name:string -> packing:(GObj.widget -> unit) -> unit ->
- GSourceView2.source_view
+ GSourceView.source_view
(** Build a new source viewer. *)
-val buffer : unit -> GSourceView2.source_buffer
+val buffer : unit -> GSourceView.source_buffer
(** @return the buffer displaying the pretty-printed AST. *)
diff --git a/src/plugins/gui/wfile.ml b/src/plugins/gui/wfile.ml
index b32f0aa306380ab548345e8716db3e0bb9eff4eb..3f6a539d468f0e04d771a6e83b5a94406eb41698 100644
--- a/src/plugins/gui/wfile.ml
+++ b/src/plugins/gui/wfile.ml
@@ -77,7 +77,8 @@ class button ?kind ?title ?select ?tooltip ?parent () =
let fld = GMisc.label ~text:"(none)" ~xalign:0.0
~packing:(box#pack ~expand:true) () in
let _ = GMisc.separator `VERTICAL
- ~packing:(box#pack ~expand:false ~padding:2) ~show:true () in
+ ~packing:(box#pack ~expand:false ~padding:2) ~show:true ()
+ in
let _ = GMisc.image ~packing:(box#pack ~expand:false) ~stock:`OPEN () in
let button = GButton.button () in
let dialog = new dialog ?kind ?title ?select ?parent () in
diff --git a/src/plugins/gui/widget.ml b/src/plugins/gui/widget.ml
index bc9c1f649ce8d4077079dcd9d95f2c66d67727b7..94e6fd1daed1f6a960bffc179f8a60207420e866 100644
--- a/src/plugins/gui/widget.ml
+++ b/src/plugins/gui/widget.ml
@@ -73,8 +73,8 @@ class label ?(style=`Label) ?(align=`Left) ?width ?text () =
| Some c0 , `NORMAL ->
w#misc#modify_fg [ `NORMAL , `COLOR c0 ]
| None , (#GDraw.color as c) ->
- fg <- Some (w#misc#style#fg `NORMAL) ;
- w#misc#modify_fg [ `NORMAL , c ]
+ fg <- Some (w#misc#style#fg `NORMAL) ;
+ w#misc#modify_fg [ `NORMAL , c ]
| Some _ , (#GDraw.color as c) ->
w#misc#modify_fg [ `NORMAL , c ]
@@ -84,8 +84,8 @@ class label ?(style=`Label) ?(align=`Left) ?width ?text () =
| Some c0 , `NORMAL ->
w#misc#modify_bg [ `NORMAL , `COLOR c0 ]
| None , (#GDraw.color as c) ->
- bg <- Some (w#misc#style#bg `NORMAL) ;
- w#misc#modify_bg [ `NORMAL , c ]
+ bg <- Some (w#misc#style#bg `NORMAL) ;
+ w#misc#modify_bg [ `NORMAL , c ]
| Some _ , (#GDraw.color as c) ->
w#misc#modify_bg [ `NORMAL , c ]
@@ -428,7 +428,7 @@ class popup () =
method add_item ~label ~callback =
if not empty && separator then
- ignore (GMenu.separator_item ~packing:menu#append ()) ;
+ ignore (GMenu.separator_item ~packing:menu#append ());
let item = GMenu.menu_item ~label ~packing:menu#append () in
ignore (item#connect#activate ~callback) ;
empty <- false ; separator <- false
diff --git a/src/plugins/gui/wpane.ml b/src/plugins/gui/wpane.ml
index 582ded99e873539e52573aef07d1967472eefb90..0f80fe87c68ee11f53589b74905d4255ee6fae33 100644
--- a/src/plugins/gui/wpane.ml
+++ b/src/plugins/gui/wpane.ml
@@ -217,7 +217,7 @@ class ['a] dialog ~title ~window ?(resize=false) () =
let shell = GWindow.window
~title ~kind:`TOPLEVEL ~modal:true
~show:false ~decorated:true ~position:`CENTER_ON_PARENT
- ~allow_grow:resize ()
+ ~resizable:resize ()
in
let hclip = GBin.alignment ~packing:shell#add () in
diff --git a/src/plugins/impact/register_gui.ml b/src/plugins/impact/register_gui.ml
index a4a6d79740dac47aefd89442aecf8584adad557b..57ffc3c620c4d6af6ec240eff2ceee389a09fc93 100644
--- a/src/plugins/impact/register_gui.ml
+++ b/src/plugins/impact/register_gui.ml
@@ -167,9 +167,7 @@ let reason_graph_window main_window ?in_kf reason =
let height = int_of_float (float main_window#default_height *. 3. /. 4.) in
let width = int_of_float (float main_window#default_width *. 3. /. 4.) in
let window =
- GWindow.window
- ~width ~height ~allow_shrink:true ~allow_grow:true
- ~position:`CENTER ()
+ GWindow.window ~width ~height ~resizable:true ~position:`CENTER ()
in
let view = reason_graph ~packing:window#add in
window#show ();
diff --git a/src/plugins/value/gui_files/gui_callstacks_manager.ml b/src/plugins/value/gui_files/gui_callstacks_manager.ml
index 2d6a51bb4e7065d60798c25627b6407439db3676..5aee78ab18b849130842d6efd3d045a05105ebe6 100644
--- a/src/plugins/value/gui_files/gui_callstacks_manager.ml
+++ b/src/plugins/value/gui_files/gui_callstacks_manager.ml
@@ -326,7 +326,6 @@ module Make (Input: Input) = struct
list_mem equal_column_type col_type model.hidden_columns
then
let show = GMenu.check_menu_item ~label:txt () in
- show#set_show_toggle true;
show#set_active column#visible;
(* Hide this column. Keep it alive for filters and co. *)
let callback_show_hide () =
@@ -354,8 +353,7 @@ module Make (Input: Input) = struct
let _lbl = GMisc.label ~text ~packing:h#pack () in
let icon = GMisc.image ~xpad:10 ~stock:`COLOR_PICKER ~packing:h#pack () in
icon#misc#hide ();
- let tooltip_before = GData.tooltips () in
- tooltip_before#set_tip ~text:tooltip h#coerce;
+ Gtk_helper.do_tooltip ~tooltip h;
(* set_widget forces Gtk to create a header button for the view_column. *)
col#set_widget (Some h#coerce);
icon
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 40d95b6abbc3f257325e9eee710777eba8f8f86a..5eb302348dd2bb65acfdd50dfc2e2d599008ef23 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -74,7 +74,12 @@ class pane (proverpane : GuiConfig.provers) =
let composer = new GuiComposer.composer printer in
let browser = new GuiComposer.browser printer in
let layout = new Wutil.layout in
+ let scroll_palette =
+ GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`NEVER ()
+ in
+ let scroll_palette_widget = new Wutil.gobj_widget scroll_palette in
let palette = new Wpalette.panel () in
+ let () = scroll_palette#add palette#coerce in
let help = new Widget.button
~label:"Tactics" ~border:false ~tooltip:"List Available Tactics" () in
let delete = new Widget.button
@@ -107,7 +112,7 @@ class pane (proverpane : GuiConfig.provers) =
w autofocus ; w play_script ; w save_script ;
w ~padding:6 icon ; h ~padding:6 status ]
[ w help ; w delete ]) in
- layout#populate (Wbox.panel ~top:toolbar ~right:palette#widget text) ;
+ layout#populate (Wbox.panel ~top:toolbar ~right:scroll_palette_widget text) ;
provers <-
VCS.([ new GuiProver.prover ~console:text ~prover:AltErgo ] @
List.map
diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index e9e2f4c1a6b64e522db79493239668fb11ece380..06f0f9d9cd53d81d56d525f00678243f669099b2 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/src/plugins/wp/GuiPanel.ml
@@ -167,7 +167,7 @@ class model_selector (main : Design.main_window_extension_points) =
let wp_dir = ref (Sys.getcwd())
let wp_script () =
- let file = GToolbox.select_file
+ let file = Gtk_helper.select_file
~title:"Script File for Coq proofs"
~dir:wp_dir ~filename:"wp.script" ()
in
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 81575977d66bab822094aaa11fcd3d1be5e5ba8e..f87cabc6d970a626c0c9529bb4e2c644dae42188 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -40,7 +40,7 @@ include $(PLUGIN_DIR)/share/Makefile.resources
# Extension of the GUI for wp is compilable
# only if gnomecanvas is available
-ifeq ($(HAS_GNOMECANVAS),yes)
+#ifeq ($(HAS_GNOMECANVAS),yes)
PLUGIN_GUI_CMO:= \
GuiConfig \
GuiList \
@@ -53,7 +53,7 @@ PLUGIN_GUI_CMO:= \
GuiSource \
GuiPanel \
GuiNavigator
-endif
+#endif
PLUGIN_ENABLE:=@ENABLE_WP@
PLUGIN_NAME:=Wp