From f3ccaf7b094bce98b309263aac862413bbb86b2d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 9 Dec 2018 20:33:46 +0100
Subject: Configuration: expand a version number to three fields when only 1 or
 2 fields are given.

---
 configure.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/configure.ml b/configure.ml
index 8b6fccb5e3..266abdf3b9 100644
--- a/configure.ml
+++ b/configure.ml
@@ -150,7 +150,10 @@ let numeric_prefix_list s =
   let max = String.length s in
   let i = ref 0 in
   while !i < max && isnum s.[!i] do incr i done;
-  string_split '.' (String.sub s 0 !i)
+  match string_split '.' (String.sub s 0 !i) with
+  | [v] -> [v;"0";"0"]
+  | [v1;v2] -> [v1;v2;"0"]
+  | v -> v
 
 (** Combined existence and directory tests *)
 
-- 
cgit v1.2.3


From 1e76c9f840135d6445e89090fcd3c6c073115a15 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 12 Nov 2018 07:52:44 +0100
Subject: CoqIDE: Replacing Tooltips with gtk+3 compliant Tooltip.

---
 ide/configwin_ihm.ml   | 92 ++++++++++++++++----------------------------------
 ide/configwin_types.ml |  2 +-
 2 files changed, 31 insertions(+), 63 deletions(-)

diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml
index 8420d930d5..e136c03e60 100644
--- a/ide/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
@@ -27,6 +27,10 @@
 
 open Configwin_types
 
+let set_help_tip wev = function
+  | None -> ()
+  | Some help -> GtkBase.Widget.Tooltip.set_text wev#as_widget help
+
 let modifiers_to_string m =
   let rec iter m s =
     match m with
@@ -71,7 +75,6 @@ class ['a] list_selection_box
     f_color
     (eq : 'a -> 'a -> bool)
     add_function title editable
-    (tt:GData.tooltips)
     =
   let _ = dbg "list_selection_box" in
   let wev = GBin.event_box () in
@@ -94,12 +97,8 @@ class ['a] list_selection_box
 	~titles_show: true
 	~packing: wscroll#add ()
   in
-  let _ =
-    match help_opt with
-      None -> ()
-    | Some help ->
-	tt#set_tip ~text: help ~privat: help wev#coerce
-  in  (* the vbox for the buttons *)
+  let _ = set_help_tip wev help_opt in
+  (* the vbox for the buttons *)
   let vbox_buttons = GPack.vbox () in
   let _ =
     if editable then
@@ -280,9 +279,8 @@ class ['a] list_selection_box
       self#update !listref
   end;;
 
-
 (** This class is used to build a box for a string parameter.*)
-class string_param_box param (tt:GData.tooltips) =
+class string_param_box param =
   let _ = dbg "string_param_box" in
   let hbox = GPack.hbox () in
   let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
@@ -292,12 +290,7 @@ class string_param_box param (tt:GData.tooltips) =
       ~packing: (hbox#pack ~expand: param.string_expand ~padding: 2)
       ()
   in
-  let _ =
-    match param.string_help with
-      None -> ()
-    | Some help ->
-	tt#set_tip ~text: help ~privat: help wev#coerce
-  in
+  let _ = set_help_tip wev param.string_help in
   let _ = we#set_text (param.string_to_string param.string_value) in
 
   object (self)
@@ -316,17 +309,12 @@ class string_param_box param (tt:GData.tooltips) =
   end ;;
 
 (** This class is used to build a box for a combo parameter.*)
-class combo_param_box param (tt:GData.tooltips) =
+class combo_param_box param =
     let _ = dbg "combo_param_box" in
     let hbox = GPack.hbox () in
     let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
     let _wl = GMisc.label ~text: param.combo_label ~packing: wev#add () in
-    let _ =
-      match param.combo_help with
-	  None -> ()
-	| Some help ->
-	    tt#set_tip ~text: help ~privat: help wev#coerce
-    in
+    let _ = set_help_tip wev param.combo_help in
     let get_value = if not param.combo_new_allowed then
       let wc = GEdit.combo_box_text
 	~strings: param.combo_choices
@@ -341,13 +329,13 @@ class combo_param_box param (tt:GData.tooltips) =
 	fun () -> match GEdit.text_combo_get_active wc with |None -> "" |Some s -> s
     else
       let (wc,_) = GEdit.combo_box_entry_text
-	~strings: param.combo_choices
-	~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
-	()
+       ~strings: param.combo_choices
+       ~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
+       ()
       in
       let _ = wc#entry#set_editable param.combo_editable in
       let _ = wc#entry#set_text param.combo_value in
-	fun () -> wc#entry#text
+       fun () -> wc#entry#text
     in
 object (self)
 
@@ -365,7 +353,7 @@ object (self)
 end ;;
 
 (** Class used to pack a custom box. *)
-class custom_param_box param (tt:GData.tooltips) =
+class custom_param_box param =
   let _ = dbg "custom_param_box" in
   let top =
     match param.custom_framed with
@@ -381,7 +369,7 @@ class custom_param_box param (tt:GData.tooltips) =
   end
 
 (** This class is used to build a box for a text parameter.*)
-class text_param_box param (tt:GData.tooltips) =
+class text_param_box param =
   let _ = dbg "text_param_box" in
   let wf = GBin.frame ~label: param.string_label ~height: 100 () in
   let wev = GBin.event_box ~packing: wf#add () in
@@ -395,12 +383,7 @@ class text_param_box param (tt:GData.tooltips) =
       ~packing: wscroll#add
       ()
   in
-  let _ =
-    match param.string_help with
-      None -> ()
-    | Some help ->
-	tt#set_tip ~text: help ~privat: help wev#coerce
-  in
+  let _ = set_help_tip wev param.string_help in
   let _ = dbg "text_param_box: buffer creation" in
   let buffer = GText.buffer () in
 
@@ -427,17 +410,13 @@ class text_param_box param (tt:GData.tooltips) =
   end ;;
 
 (** This class is used to build a box for a boolean parameter.*)
-class bool_param_box param (tt:GData.tooltips) =
+class bool_param_box param =
   let _ = dbg "bool_param_box" in
   let wchk = GButton.check_button
       ~label: param.bool_label
       ()
   in
-  let _ =
-    match param.bool_help with
-      None -> ()
-    | Some help -> tt#set_tip ~text: help ~privat: help wchk#coerce
-  in
+  let _ = set_help_tip wchk param.bool_help in
   let _ = wchk#set_active param.bool_value in
   let _ = wchk#misc#set_sensitive param.bool_editable in
 
@@ -471,14 +450,7 @@ class modifiers_param_box param =
                                  else value := List.filter ((<>) modifier) !value)))
             param.md_allow
   in
-  let _ =
-    match param.md_help with
-      None -> ()
-    | Some help ->
-       let tooltips = GData.tooltips () in
-       ignore (hbox#connect#destroy ~callback: tooltips#destroy);
-       tooltips#set_tip wev#coerce ~text: help ~privat: help
-  in
+  let _ = set_help_tip wev param.md_help in
   object (self)
 
     (** This method returns the main box ready to be packed. *)
@@ -495,7 +467,7 @@ class modifiers_param_box param =
   end ;;
 
 (** This class is used to build a box for a parameter whose values are a list.*)
-class ['a] list_param_box (param : 'a list_param) (tt:GData.tooltips) =
+class ['a] list_param_box (param : 'a list_param) =
   let _ = dbg "list_param_box" in
   let listref = ref param.list_value in
   let frame_selection = new list_selection_box
@@ -522,7 +494,7 @@ class ['a] list_param_box (param : 'a list_param) (tt:GData.tooltips) =
   end ;;
 
 (** This class creates a configuration box from a configuration structure *)
-class configuration_box (tt : GData.tooltips) conf_struct =
+class configuration_box conf_struct =
 
   let main_box = GPack.hbox () in
 
@@ -553,27 +525,27 @@ class configuration_box (tt : GData.tooltips) conf_struct =
 
   let make_param (main_box : #GPack.box) = function
   | String_param p ->
-    let box = new string_param_box p tt in
+    let box = new string_param_box p in
     let _ = main_box#pack ~expand: false ~padding: 2 box#box in
     box
   | Combo_param p ->
-    let box = new combo_param_box p tt in
+    let box = new combo_param_box p in
     let _ = main_box#pack ~expand: false ~padding: 2 box#box in
     box
   | Text_param p ->
-    let box = new text_param_box p tt in
+    let box = new text_param_box p in
     let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in
     box
   | Bool_param p ->
-    let box = new bool_param_box p tt in
+    let box = new bool_param_box p in
     let _ = main_box#pack ~expand: false ~padding: 2 box#box in
     box
   | List_param f ->
-    let box = f tt in
+    let box = f () in
     let _ = main_box#pack ~expand: true ~padding: 2 box#box in
     box
   | Custom_param p ->
-    let box = new custom_param_box p tt in
+    let box = new custom_param_box p in
     let _ = main_box#pack ~expand: p.custom_expand ~padding: 2 box#box in
     box
   | Modifiers_param p ->
@@ -684,9 +656,7 @@ let edit ?(with_apply=true)
     ?parent ?height ?width
     ()
   in
-  let tooltips = GData.tooltips () in
-
-  let config_box = new configuration_box tooltips conf_struct in
+  let config_box = new configuration_box conf_struct in
 
   let _ = dialog#vbox#add config_box#box#coerce in
 
@@ -697,7 +667,6 @@ let edit ?(with_apply=true)
   dialog#add_button Configwin_messages.mCancel `CANCEL;
 
   let destroy () =
-    tooltips#destroy () ;
     dialog#destroy ();
   in
   let rec iter rep =
@@ -753,7 +722,7 @@ let list ?(editable=true) ?help
     ?titles ?(color=(fun (_:'a) -> (None : string option)))
     label (f_strings : 'a -> string list) v =
   List_param
-    (fun tt ->
+    (fun () ->
 	new list_param_box
 	  {
 	    list_label = label ;
@@ -768,7 +737,6 @@ let list ?(editable=true) ?help
 	    list_f_add = add ;
 	    list_f_apply = f ;
 	  }
-	  tt
     )
 
 (** Create a strings param. *)
diff --git a/ide/configwin_types.ml b/ide/configwin_types.ml
index 9e339d135d..251e3dded3 100644
--- a/ide/configwin_types.ml
+++ b/ide/configwin_types.ml
@@ -97,7 +97,7 @@ type modifiers_param = {
 (** This type represents the different kinds of parameters. *)
 type parameter_kind =
     String_param of string string_param
-  | List_param of (GData.tooltips -> <box: GObj.widget ; apply : unit>)
+  | List_param of (unit -> <box: GObj.widget ; apply : unit>)
   | Bool_param of bool_param
   | Text_param of string string_param
   | Combo_param of combo_param
-- 
cgit v1.2.3


From 977261ed0afd415932401c3f5df258333488e47b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 15:39:37 +0100
Subject: CoqIDE: Adapt configuration to require lablgtk3 and gtksourceview3.

---
 INSTALL                             |  4 ++--
 Makefile.ide                        | 10 +++++-----
 configure.ml                        | 36 +++++++++++++-----------------------
 coqide.opam                         |  4 ++--
 dev/ci/docker/bionic_coq/Dockerfile |  6 +++---
 ide/dune                            |  2 +-
 6 files changed, 26 insertions(+), 36 deletions(-)

diff --git a/INSTALL b/INSTALL
index 44ea195f59..e02439c54b 100644
--- a/INSTALL
+++ b/INSTALL
@@ -43,8 +43,8 @@ WHAT DO YOU NEED ?
 
    - a C compiler
 
-   - for CoqIDE, the lablgtk development files (version >= 2.18.5),
-     and the GTK 2.x libraries including gtksourceview2.
+   - for CoqIDE, the lablgtk development files (version >= 3.0.0),
+     and the GTK 3.x libraries including gtksourceview3.
 
    Note that num and lablgtk should be properly registered with
    findlib/ocamlfind as Coq's makefile will use it to locate the
diff --git a/Makefile.ide b/Makefile.ide
index db1cc3746d..86bdaf62d4 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -17,7 +17,7 @@
 
 ## Coqide-related variables set by ./configure in config/Makefile
 
-#COQIDEINCLUDES : something like -I +lablgtk2
+#COQIDEINCLUDES : something like -I +lablgtk3
 #HASCOQIDE : opt / byte / no
 #IDEFLAGS : some extra cma, for instance
 #IDEOPTCDEPS : on windows, ide/ide_win32_stubs.o ide/coq_icon.o
@@ -98,7 +98,7 @@ ifeq ($(HASCOQIDE),opt)
 $(COQIDE): $(LINKIDEOPT)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
-	       -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^
+	       -linkpkg -package str,unix,dynlink,threads,lablgtk3.sourceview3 $(IDEFLAGS:.cma=.cmxa) $^
 	$(STRIP_HIDE) $@
 else
 $(COQIDE): $(COQIDEBYTE)
@@ -108,7 +108,7 @@ endif
 $(COQIDEBYTE): $(LINKIDE)
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \
-	       -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
+	       -linkpkg -package str,unix,dynlink,threads,lablgtk3.sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
 
 ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile
 	@rm -f $@
@@ -128,7 +128,7 @@ ide/%.cmx: ide/%.ml
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
 
 # We need to compile this file without -safe-string due mess with
-# lablgtk API. Other option is to require lablgtk >= 2.8.16
+# lablgtk API. Other option is to require lablgtk >= 3.0.0
 ide/ideutils.cmo: ide/ideutils.ml
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(filter-out -safe-string,$(OCAMLC)) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
@@ -228,7 +228,7 @@ $(COQIDEAPP)/Contents:
 $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
-	        -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^
+	        -linkpkg -package str,unix,dynlink,threads,lablgtk3.sourceview3 $(IDEFLAGS:.cma=.cmxa) $^
 	$(STRIP_HIDE) $@
 
 $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
diff --git a/configure.ml b/configure.ml
index 266abdf3b9..14698c4e61 100644
--- a/configure.ml
+++ b/configure.ml
@@ -700,7 +700,7 @@ let check_for_numlib () =
 let numlib =
   check_for_numlib ()
 
-(** * lablgtk2 and CoqIDE *)
+(** * lablgtk3 and CoqIDE *)
 
 type source = Manual | OCamlFind | Stdlib
 
@@ -716,7 +716,7 @@ let check_lablgtkdir ?(fatal=false) src dir =
   let msg = get_source src in
   if not (dir_exists dir) then
     yell (sprintf "No such directory '%s' (%s)." dir msg)
-  else if not (Sys.file_exists (dir/"gSourceView2.cmi")) then
+  else if not (Sys.file_exists (dir/"gSourceView2.cmi") || Sys.file_exists (dir/"gSourceView3.cmi")) then
     yell (sprintf "Incomplete LablGtk2 (%s): no %s/gSourceView2.cmi." msg dir)
   else if not (Sys.file_exists (dir/"glib.mli")) then
     yell (sprintf "Incomplete LablGtk2 (%s): no %s/glib.mli." msg dir)
@@ -732,15 +732,15 @@ let get_lablgtkdir () =
     else "", msg
   | None ->
     let msg = OCamlFind in
-    let d1,_ = tryrun camlexec.find ["query";"lablgtk2.sourceview2"] in
+    let d1,_ = tryrun camlexec.find ["query";"lablgtk3.sourceview3"] in
     if d1 <> "" && check_lablgtkdir msg d1 then d1, msg
     else
-      (* In debian wheezy, ocamlfind knows only of lablgtk2 *)
-      let d2,_ = tryrun camlexec.find ["query";"lablgtk2"] in
+      (* In debian wheezy, ocamlfind knows only of lablgtk3 *)
+      let d2,_ = tryrun camlexec.find ["query";"lablgtk3"] in
       if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg
       else
         let msg = Stdlib in
-        let d3 = camllib^"/lablgtk2" in
+        let d3 = camllib^"/lablgtk3" in
         if check_lablgtkdir msg d3 then d3, msg
         else "", msg
 
@@ -748,24 +748,14 @@ let get_lablgtkdir () =
 
 let check_lablgtk_version src dir = match src with
 | Manual | Stdlib ->
-  warn "Could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.";
+  warn "Could not check the version of lablgtk3.\nMake sure your version is at least 3.0.0.";
   (true, "an unknown version")
 | OCamlFind ->
-  let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in
+  let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk3"] in
   try
     let vi = List.map s2i (numeric_prefix_list v) in
-    if vi < [2; 16; 0] then
+    if vi < [3; 0; 0] then
       (false, v)
-    else if vi < [2; 18; 3] then
-      begin
-        (* Version 2.18.3 is known to report incorrectly as 2.18.0, and Launchpad packages report as version 2.16.0 due to a misconfigured META file; see https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 *)
-        warn "Your installed lablgtk reports as %s.\n\
-It is possible that the installed version is actually more recent\n\
-but reports an incorrect version. If the installed version is\n\
-actually more recent than 2.18.3, that's fine; if it is not,\n
-CoqIDE will compile but may be very unstable." v;
-        (true, "an unknown version")
-      end
     else
       (true, v)
   with _ -> (false, v)
@@ -791,10 +781,10 @@ let lablgtkdir = ref ""
 let check_coqide () =
   if !prefs.coqide = Some No then set_ide No "CoqIde manually disabled";
   let dir, via = get_lablgtkdir () in
-  if dir = "" then set_ide No "LablGtk2 not found";
+  if dir = "" then set_ide No "LablGtk3 not found";
   let (ok, version) = check_lablgtk_version via dir in
-  let found = sprintf "LablGtk2 found (%s, %s)" (get_source via) version in
-  if not ok then set_ide No (found^", but too old (required >= 2.18.3, found " ^ version ^ ")");
+  let found = sprintf "LablGtk3 found (%s, %s)" (get_source via) version in
+  if not ok then set_ide No (found^", but too old (required >= 3.0, found " ^ version ^ ")");
   (* We're now sure to produce at least one kind of coqide *)
   lablgtkdir := shorten_camllib dir;
   if !prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested");
@@ -1014,7 +1004,7 @@ let print_summary () =
   if best_compiler = "opt" then
     pr "  Native dynamic link support : %B\n" hasnatdynlink;
   if coqide <> "no" then
-    pr "  Lablgtk2 library in         : %s\n" (esc !lablgtkdir);
+    pr "  Lablgtk3 library in         : %s\n" (esc !lablgtkdir);
   if !idearchdef = "QUARTZ" then
     pr "  Mac OS integration is on\n";
   pr "  CoqIde                      : %s\n" coqide;
diff --git a/coqide.opam b/coqide.opam
index 314943a881..9e22091898 100644
--- a/coqide.opam
+++ b/coqide.opam
@@ -19,8 +19,8 @@ license: "LGPL-2.1"
 depends: [
   "dune"               { build & >= "1.4.0" }
   "coqide-server"
-  "conf-gtksourceview"
-  "lablgtk"            {         >= "2.18.5" }
+  "conf-gtksourceview3"
+  "lablgtk3"
 ]
 
 build-env: [
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index ac763547b6..c95bcf5573 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -10,7 +10,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         # Dependencies of the image, the test-suite and external projects
         m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \
         # Dependencies of lablgtk (for CoqIDE)
-        libgtk2.0-dev libgtksourceview2.0-dev \
+        libgtk3.0-dev libgtksourceview3.0-dev \
         # Dependencies of stdlib and sphinx doc
         texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
         xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \
@@ -41,7 +41,7 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \
     CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
-ENV COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
+ENV COQIDE_OPAM="lablgtk3 conf-gtksourceview3"
 
 # base switch
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
@@ -53,7 +53,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.07.1" \
-    COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
+    COQIDE_OPAM_EDGE="lablgtk3 conf-gtksourceview3" \
     BASE_OPAM_EDGE="dune-release.1.1.0"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
diff --git a/ide/dune b/ide/dune
index 3618e4f05d..5082d84c4f 100644
--- a/ide/dune
+++ b/ide/dune
@@ -29,7 +29,7 @@
  (wrapped false)
  (modules (:standard \ document fake_ide idetop coqide_main))
  (optional)
- (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2))
+ (libraries coqide-server.protocol coqide-server.core lablgtk3.sourceview3))
 
 (rule
  (targets coqide_os_specific.ml)
-- 
cgit v1.2.3


From d016e542bb42c2b47f9cfc66f51cd01d52124141 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 15:57:59 +0100
Subject: CoqIDE: Change name of module: Sourceview2 -> Sourceview3

---
 ide/nanoPG.ml         |  2 +-
 ide/preferences.ml    |  4 ++--
 ide/preferences.mli   |  4 ++--
 ide/session.ml        |  2 +-
 ide/wg_MessageView.ml |  4 ++--
 ide/wg_ProofView.ml   |  4 ++--
 ide/wg_ScriptView.ml  | 14 +++++++-------
 ide/wg_ScriptView.mli |  8 ++++----
 8 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml
index f2913b1d1d..d85d87142c 100644
--- a/ide/nanoPG.ml
+++ b/ide/nanoPG.ml
@@ -52,7 +52,7 @@ let pr_key t =
 type action =
   | Action of string * string
   | Callback of (gui -> unit)
-  | Edit of (status -> GSourceView2.source_buffer -> GText.iter ->
+  | Edit of (status -> GSourceView3.source_buffer -> GText.iter ->
               (string -> string -> unit) -> status)
   | Motion of (status -> GText.iter -> GText.iter * status)
 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index fb0eea1405..1f4b9ced2d 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -12,10 +12,10 @@ open Configwin
 
 let pref_file = Filename.concat (Minilib.coqide_config_home ()) "coqiderc"
 let accel_file = Filename.concat (Minilib.coqide_config_home ()) "coqide.keys"
-let lang_manager = GSourceView2.source_language_manager ~default:true
+let lang_manager = GSourceView3.source_language_manager ~default:true
 let () = lang_manager#set_search_path
   ((Minilib.coqide_data_dirs ())@lang_manager#search_path)
-let style_manager = GSourceView2.source_style_scheme_manager ~default:true
+let style_manager = GSourceView3.source_style_scheme_manager ~default:true
 let () = style_manager#set_search_path
   ((Minilib.coqide_data_dirs ())@style_manager#search_path)
 
diff --git a/ide/preferences.mli b/ide/preferences.mli
index cf2265781c..7de38c651d 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -8,8 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val lang_manager : GSourceView2.source_language_manager
-val style_manager : GSourceView2.source_style_scheme_manager
+val lang_manager : GSourceView3.source_language_manager
+val style_manager : GSourceView3.source_style_scheme_manager
 
 type project_behavior = Ignore_args | Append_args | Subst_args
 type inputenc = Elocale | Eutf8 | Emanual of string
diff --git a/ide/session.ml b/ide/session.ml
index e2427a9b51..b7f98f3d79 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -47,7 +47,7 @@ type session = {
 }
 
 let create_buffer () =
-  let buffer = GSourceView2.source_buffer
+  let buffer = GSourceView3.source_buffer
     ~tag_table:Tags.Script.table
     ~highlight_matching_brackets:true
     ?language:(lang_manager#language source_language#get)
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 6b09b344b5..b302cbc066 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -42,7 +42,7 @@ class type message_view =
   end
 
 let message_view () : message_view =
-  let buffer = GSourceView2.source_buffer
+  let buffer = GSourceView3.source_buffer
     ~highlight_matching_brackets:true
     ~tag_table:Tags.Message.table ()
   in
@@ -50,7 +50,7 @@ let message_view () : message_view =
   let box = GPack.vbox () in
   let scroll = GBin.scrolled_window
     ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(box#pack ~expand:true) () in
-  let view = GSourceView2.source_view
+  let view = GSourceView3.source_view
     ~source_buffer:buffer ~packing:scroll#add
     ~editable:false ~cursor_visible:false ~wrap_mode:`WORD ()
   in
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 9be562d3ed..7894ded532 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -193,12 +193,12 @@ let display mode (view : #GText.view_skel) goals hints evars =
 
 
 let proof_view () =
-  let buffer = GSourceView2.source_buffer
+  let buffer = GSourceView3.source_buffer
     ~highlight_matching_brackets:true
     ~tag_table:Tags.Proof.table ()
   in
   let text_buffer = new GText.buffer buffer#as_buffer in
-  let view = GSourceView2.source_view
+  let view = GSourceView3.source_view
     ~source_buffer:buffer ~editable:false ~wrap_mode:`WORD ()
   in
   let () = Gtk_parsing.fix_double_click view in
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 5e26c50797..8677f5fc65 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -284,12 +284,12 @@ end
 
 class script_view (tv : source_view) (ct : Coq.coqtop) =
 
-let view = new GSourceView2.source_view (Gobject.unsafe_cast tv) in
+let view = new GSourceView3.source_view (Gobject.unsafe_cast tv) in
 let completion = new Wg_Completion.complete_model ct view#buffer in
 let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in
 
 object (self)
-  inherit GSourceView2.source_view (Gobject.unsafe_cast tv)
+  inherit GSourceView3.source_view (Gobject.unsafe_cast tv)
 
   val undo_manager = new undo_manager view#buffer
 
@@ -491,17 +491,17 @@ object (self)
 
 end
 
-let script_view ct ?(source_buffer:GSourceView2.source_buffer option)  ?draw_spaces =
-  GtkSourceView2.SourceView.make_params [] ~cont:(
+let script_view ct ?(source_buffer:GSourceView3.source_buffer option)  ?draw_spaces =
+  GtkSourceView3.SourceView.make_params [] ~cont:(
     GtkText.View.make_params ~cont:(
       GContainer.pack_container ~create:
 	(fun pl ->
 	  let w = match source_buffer with
-	    | None -> GtkSourceView2.SourceView.new_ ()
-	    | Some buf -> GtkSourceView2.SourceView.new_with_buffer
+            | None -> GtkSourceView3.SourceView.new_ ()
+            | Some buf -> GtkSourceView3.SourceView.new_with_buffer
               (Gobject.try_cast buf#as_buffer "GtkSourceBuffer")
 	  in
 	  let w = Gobject.unsafe_cast w in
 	  Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
-	  Gaux.may ~f:(GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces;
+          Gaux.may ~f:(GtkSourceView3.SourceView.set_draw_spaces w) draw_spaces;
 	  ((new script_view w ct) : script_view))))
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index be6510dbe2..ef7e92ff38 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -14,7 +14,7 @@ type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj
 
 class script_view : source_view -> Coq.coqtop ->
 object
-  inherit GSourceView2.source_view
+  inherit GSourceView3.source_view
   method undo : unit -> unit
   method redo : unit -> unit
   method clear_undo : unit -> unit
@@ -31,8 +31,8 @@ object
 end
 
 val script_view : Coq.coqtop ->
-  ?source_buffer:GSourceView2.source_buffer ->
-  ?draw_spaces:SourceView2Enums.source_draw_spaces_flags list ->
+  ?source_buffer:GSourceView3.source_buffer ->
+  ?draw_spaces:SourceView3Enums.source_draw_spaces_flags list ->
   ?auto_indent:bool ->
   ?highlight_current_line:bool ->
   ?indent_on_tab:bool ->
@@ -42,7 +42,7 @@ val script_view : Coq.coqtop ->
   ?show_line_marks:bool ->
   ?show_line_numbers:bool ->
   ?show_right_margin:bool ->
-  ?smart_home_end:SourceView2Enums.source_smart_home_end_type ->
+  ?smart_home_end:SourceView3Enums.source_smart_home_end_type ->
   ?tab_width:int ->
   ?editable:bool ->
   ?cursor_visible:bool ->
-- 
cgit v1.2.3


From bcbeac04993ffbad4f4432b646614491f2d8a5d5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 15:56:29 +0100
Subject: CoqIDE: Ensuring that gtk is initialized before other inits done in
 ideutils.ml.

This seems fragile: does it depend on the order files are loaded? (It
was working for gtk2 when gtk initialization was in coqide_main.ml but
it does not work anymore for CoqIDE built on gtk3).

Eventually, it might be needed to centralize all initialization side
effects in one place.
---
 ide/coqide_main.ml | 2 +-
 ide/ideutils.ml    | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/ide/coqide_main.ml b/ide/coqide_main.ml
index 21f513b8f4..79420b3857 100644
--- a/ide/coqide_main.ml
+++ b/ide/coqide_main.ml
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-let _ = GtkMain.Main.init ()
+let _ = Coqide.set_signal_handlers ()
 
 (* We handle Gtk warning messages ourselves :
    - on win32, we don't want them to end on a non-existing console
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 5beaba3604..7a44d21ecf 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -8,9 +8,10 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-
 open Preferences
 
+let _ = GtkMain.Main.init ()
+
 let warn_image () =
   let img = GMisc.image () in
   img#set_stock `DIALOG_WARNING;
-- 
cgit v1.2.3


From 06fc3fa551aeb53fbe06acad5d42b61201927c22 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 17:16:18 +0100
Subject: CoqIDE: Deactiving the list and string configuration tools.

They rely on gtk2 clist and would need to be changed to list_store.
---
 ide/configwin.ml      |  2 ++
 ide/configwin.mli     |  2 ++
 ide/configwin_ihm.ml  | 10 ++++++++--
 ide/configwin_ihm.mli |  2 ++
 4 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/ide/configwin.ml b/ide/configwin.ml
index 24be721631..79a1eae880 100644
--- a/ide/configwin.ml
+++ b/ide/configwin.ml
@@ -37,8 +37,10 @@ type return_button =
   | Return_cancel
 
 let string = Configwin_ihm.string
+(*
 let strings = Configwin_ihm.strings
 let list = Configwin_ihm.list
+*)
 let bool = Configwin_ihm.bool
 let combo = Configwin_ihm.combo
 let custom = Configwin_ihm.custom
diff --git a/ide/configwin.mli b/ide/configwin.mli
index 0ee77d69b5..fa22846d19 100644
--- a/ide/configwin.mli
+++ b/ide/configwin.mli
@@ -69,6 +69,7 @@ val string : ?editable: bool -> ?expand: bool -> ?help: string ->
 val bool : ?editable: bool -> ?help: string ->
   ?f: (bool -> unit) -> string -> bool -> parameter_kind
 
+(*
 (** [strings label value] creates a string list parameter.
    @param editable indicate if the value is editable (default is [true]).
    @param help an optional help message.
@@ -119,6 +120,7 @@ val list : ?editable: bool -> ?help: string ->
 		('a -> string list) ->
 		  'a list ->
 		    parameter_kind
+*)
 
 (** [combo label choices value] creates a combo parameter.
    @param editable indicate if the value is editable (default is [true]).
diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml
index e136c03e60..9fe3d8bb35 100644
--- a/ide/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
@@ -59,7 +59,7 @@ class type widget =
 
 let debug = false
 let dbg s = if debug then Minilib.log s else ()
-
+(*
 (** This class builds a frame with a clist and two buttons :
    one to add items and one to remove the selected items.
    The class takes in parameter a function used to add items and
@@ -278,6 +278,7 @@ class ['a] list_selection_box
       (* initialize the clist with the listref *)
       self#update !listref
   end;;
+*)
 
 (** This class is used to build a box for a string parameter.*)
 class string_param_box param =
@@ -465,7 +466,7 @@ class modifiers_param_box param =
       else
 	()
   end ;;
-
+(*
 (** This class is used to build a box for a parameter whose values are a list.*)
 class ['a] list_param_box (param : 'a list_param) =
   let _ = dbg "list_param_box" in
@@ -492,6 +493,7 @@ class ['a] list_param_box (param : 'a list_param) =
       param.list_f_apply !listref ;
       param.list_value <- !listref
   end ;;
+*)
 
 (** This class creates a configuration box from a configuration structure *)
 class configuration_box conf_struct =
@@ -683,10 +685,12 @@ let edit ?(with_apply=true)
   in
     iter Return_cancel
 
+(*
 let edit_string l s =
   match GToolbox.input_string ~title: l ~text: s Configwin_messages.mValue with
     None -> s
   | Some s2 -> s2
+*)
 
 (** Create a string param. *)
 let string ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
@@ -713,6 +717,7 @@ let bool ?(editable=true) ?help ?(f=(fun _ -> ())) label v =
       bool_f_apply = f ;
     }
 
+(*
 (** Create a list param. *)
 let list ?(editable=true) ?help
     ?(f=(fun (_:'a list) -> ()))
@@ -745,6 +750,7 @@ let strings ?(editable=true) ?help
     ?(eq=Pervasives.(=))
     ?(add=(fun () -> [])) label v =
   list ~editable ?help ~f ~eq ~edit: (edit_string label) ~add label (fun s -> [s]) v
+*)
 
 (** Create a combo param. *)
 let combo ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ()))
diff --git a/ide/configwin_ihm.mli b/ide/configwin_ihm.mli
index 772a0958ff..ce6cd4d7c1 100644
--- a/ide/configwin_ihm.mli
+++ b/ide/configwin_ihm.mli
@@ -29,6 +29,7 @@ val string : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?f: (string -> unit) -> string -> string -> parameter_kind
 val bool : ?editable: bool -> ?help: string ->
   ?f: (bool -> unit) -> string -> bool -> parameter_kind
+(*
 val strings : ?editable: bool -> ?help: string ->
   ?f: (string list -> unit) ->
     ?eq: (string -> string -> bool) ->
@@ -45,6 +46,7 @@ val list : ?editable: bool -> ?help: string ->
                 ('a -> string list) ->
                   'a list ->
                     parameter_kind
+*)
 val combo : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?f: (string -> unit) ->
     ?new_allowed: bool -> ?blank_allowed: bool ->
-- 
cgit v1.2.3


From 09fb7dbd2ca87fcd64a3d6d99eb5e537aadd0c06 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 16:37:38 +0100
Subject: CoqIDE: Deactivating the user queries and wizard tactics
 configuration.

They rely on list and strings from configwin which themselves rely on
gtk2 only widgets.
---
 ide/preferences.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 1f4b9ced2d..7e53dee351 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -921,6 +921,7 @@ let configure ?(apply=(fun () -> ())) parent =
                    else cmd_browse#get])
       cmd_browse#get
   in
+(*
   let automatic_tactics =
     strings
       ~f:automatic_tactics#set
@@ -929,12 +930,14 @@ let configure ?(apply=(fun () -> ())) parent =
       automatic_tactics#get
 
   in
+*)
 
   let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in
 
   let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch;
               vertical_tabs;opposite_tabs] in
 
+(*
   let add_user_query () =
     let input_string l v =
       match GToolbox.input_string ~title:l v with
@@ -964,6 +967,7 @@ let configure ?(apply=(fun () -> ())) parent =
       user_queries#get
 
   in
+*)
 
 (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!!
    (shame on Benjamin) *)
@@ -987,12 +991,14 @@ let configure ?(apply=(fun () -> ())) parent =
      Section("Externals", None,
 	     [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
               cmd_print;cmd_editor;cmd_browse]);
+(*
      Section("Tactics Wizard", None,
 	     [automatic_tactics]);
+*)
      Section("Shortcuts", Some `PREFERENCES,
 	     [modifiers_valid; modifier_for_tactics;
         modifier_for_templates; modifier_for_display; modifier_for_navigation;
-        modifier_for_queries; user_queries]);
+        modifier_for_queries (*; user_queries *)]);
      Section("Misc", Some `ADD,
        misc)]
   in
-- 
cgit v1.2.3


From 173b5b889c306fe166ed4da5e6986e7810c7d3bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 15:43:09 +0100
Subject: CoqIDE: Moving last use of gtk2-only FileSelection to
 FileChooserDialog.

---
 ide/coq.ml       | 15 +++++++--------
 ide/ideutils.ml  |  9 ++++++---
 ide/ideutils.mli |  2 +-
 3 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/ide/coq.ml b/ide/coq.ml
index e7eea4ced2..a420a3cbf5 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -128,16 +128,15 @@ and asks_for_coqtop args =
       let () = pb_mes#destroy () in
       filter_coq_opts args
     | `DELETE_EVENT | `NO ->
-      let () = pb_mes#destroy () in
-      let cmd_sel = GWindow.file_selection
+      let file = select_file_for_open
         ~title:"coqidetop to execute (edit your preference then)"
-	~filename:(coqtop_path ()) ~urgency_hint:true () in
-      match cmd_sel#run () with
-	| `OK ->
-	  let () = custom_coqtop := (Some cmd_sel#filename) in
-	  let () = cmd_sel#destroy () in
+        ~filter:false
+        ~filename:(coqtop_path ()) () in
+      match file with
+      | Some _ ->
+          let () = custom_coqtop := file in
 	  filter_coq_opts args
-	| `CANCEL | `DELETE_EVENT | `HELP -> exit 0
+      | None -> exit 0
 
 exception WrongExitStatus of string
 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 7a44d21ecf..d0fbf796a0 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -230,14 +230,17 @@ let current_dir () = match project_path#get with
 | None -> ""
 | Some dir -> dir
 
-let select_file_for_open ~title ?filename () =
+let select_file_for_open ~title ?(filter=true) ?filename () =
   let file_chooser =
     GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title ()
   in
   file_chooser#add_button_stock `CANCEL `CANCEL ;
   file_chooser#add_select_button_stock `OPEN `OPEN ;
-  file_chooser#add_filter (filter_coq_files ());
-  file_chooser#add_filter (filter_all_files ());
+  if filter then
+    begin
+      file_chooser#add_filter (filter_coq_files ());
+      file_chooser#add_filter (filter_all_files ())
+    end;
   file_chooser#set_default_response `OPEN;
   let dir = match filename with
     | None -> current_dir ()
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 531c71cd4b..cc7d865325 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -30,7 +30,7 @@ val find_tag_limits : GText.tag -> GText.iter -> GText.iter * GText.iter
 val find_tag_start : GText.tag -> GText.iter -> GText.iter
 val find_tag_stop : GText.tag -> GText.iter -> GText.iter
 
-val select_file_for_open : title:string -> ?filename:string -> unit -> string option
+val select_file_for_open : title:string -> ?filter:bool -> ?filename:string -> unit -> string option
 val select_file_for_save :
   title:string -> ?filename:string -> unit -> string option
 val try_convert : string -> string
-- 
cgit v1.2.3


From 97f973000a11e667b0d5faef9264f4e681bbd8e1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 16:20:31 +0100
Subject: CoqIDE: Deactivation pixmap-based progression bar (wg_Segment.ml).

Indeed, gtk3 has no more Pixmap, it should use Cairo instead.

We also deactivate the functions in the graph of dependency. In
particular, this also blocks coqOps.ml.
---
 ide/coqOps.ml      |  2 ++
 ide/wg_Segment.ml  | 22 ++++++++++++++++------
 ide/wg_Segment.mli |  2 ++
 3 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 8da9900724..4aa801c2b2 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -250,6 +250,7 @@ object(self)
     feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback;
     let md = segment_model document in
     segment#set_model md;
+(*
     let on_click id =
       let find _ _ s = Int.equal s.index id in
       let sentence = Doc.find document find in
@@ -266,6 +267,7 @@ object(self)
       ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
     in
     let _ = segment#connect#clicked ~callback:on_click in
+*)
     ()
 
   method private tooltip_callback ~x ~y ~kbd tooltip =
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index 3b2572f9d2..2e5de64254 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -8,8 +8,10 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(*
 open Util
 open Preferences
+*)
 
 type color = GDraw.color
 
@@ -22,6 +24,7 @@ object
   method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a
 end
 
+(*
 let i2f = float_of_int
 let f2i = int_of_float
 
@@ -32,14 +35,14 @@ let color_eq (c1 : GDraw.color) (c2 : GDraw.color) = match c1, c2 with
 | `RGB (r1, g1, b1), `RGB (r2, g2, b2) -> r1 = r2 && g1 = g2 && b1 = b2
 | `WHITE, `WHITE -> true
 | _ -> false
-
+*)
 class type segment_signals =
 object
   inherit GObj.misc_signals
   inherit GUtil.add_ml_signals
   method clicked : callback:(int -> unit) -> GtkSignal.id
 end
-
+(*
 class segment_signals_impl obj (clicked : 'a GUtil.signal) : segment_signals =
 object
   val after = false
@@ -47,11 +50,14 @@ object
   inherit GUtil.add_ml_signals obj [clicked#disconnect]
   method clicked = clicked#connect ~after
 end
+*)
 
 class segment () =
 let box = GBin.frame () in
+(*
 let eventbox = GBin.event_box ~packing:box#add () in
 let draw = GMisc.image ~packing:eventbox#add () in
+*)
 object (self)
 
   inherit GObj.widget box#as_widget
@@ -60,11 +66,13 @@ object (self)
   val mutable height = 20
   val mutable model : model option = None
   val mutable default : color = `WHITE
+(*
   val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 ()
+*)
   val clicked = new GUtil.signal ()
   val mutable need_refresh = false
   val refresh_timer = Ideutils.mktimer ()
-
+(*
   initializer
     box#misc#set_size_request ~height ();
     let cb rect =
@@ -95,17 +103,18 @@ object (self)
     draw#set_pixmap pixmap;
     refresh_timer.Ideutils.run ~ms:300
       ~callback:(fun () -> if need_refresh then self#refresh (); true)
-
+*)
   method set_model md =
     model <- Some md;
     let changed_cb = function
     | `INSERT | `REMOVE ->
       if self#misc#visible then need_refresh <- true
     | `SET (i, color) ->
-      if self#misc#visible then self#fill_range color i (i + 1)
+      ()
+(*      if self#misc#visible then self#fill_range color i (i + 1)*)
     in
     md#changed ~callback:changed_cb
-
+(*
   method private fill_range color i j = match model with
   | None -> ()
   | Some md ->
@@ -150,5 +159,6 @@ object (self)
 
   method connect =
     new segment_signals_impl box#as_widget clicked
+*)
 
 end
diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli
index 07f545fee7..84d487f35f 100644
--- a/ide/wg_Segment.mli
+++ b/ide/wg_Segment.mli
@@ -31,7 +31,9 @@ class segment : unit ->
     inherit GObj.widget
     val obj : Gtk.widget Gtk.obj
     method set_model : model -> unit
+(*
     method connect : segment_signals
     method default_color : color
     method set_default_color : color -> unit
+*)
   end
-- 
cgit v1.2.3


From 05e15386fad28f138e6e889c421242c60b9cb39a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 15:45:05 +0100
Subject: CoqIDE: Now calling destroy signal via widget_signals.

Thanks to J. Garrigue for the hint.
---
 ide/coqide.ml       | 4 ++--
 ide/preferences.ml  | 4 ++--
 ide/preferences.mli | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 94778e0c60..0acbef1ad7 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1222,8 +1222,8 @@ let build_ui () =
   let () = GtkButton.Toolbar.set
     ~orientation:`HORIZONTAL ~style:`ICONS ~tooltips:true tbar
   in
-  let toolbar = new GObj.widget tbar in
-  let () = vbox#pack toolbar in
+  let toolbar = new GButton.toolbar tbar in
+  let () = vbox#pack toolbar#coerce in
 
   (* Emacs/PG mode *)
   NanoPG.init w notebook all_menus;
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 7e53dee351..ee274b7001 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -73,11 +73,11 @@ object (self)
   method default = default
 end
 
-let stick (pref : 'a preference) (obj : #GObj.widget as 'obj)
+let stick (pref : 'a preference) (obj : < connect : #GObj.widget_signals ; .. >)
   (cb : 'a -> unit) =
   let _ = cb pref#get in
   let p_id = pref#connect#changed ~callback:(fun v -> cb v) in
-  let _ = obj#misc#connect#destroy ~callback:(fun () -> pref#connect#disconnect p_id) in
+  let _ = obj#connect#destroy ~callback:(fun () -> pref#connect#disconnect p_id) in
   ()
 
 (** Useful marshallers *)
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 7de38c651d..8745c2ae91 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -108,6 +108,6 @@ val load_pref : unit -> unit
 val configure : ?apply:(unit -> unit) -> GWindow.window -> unit
 
 val stick : 'a preference ->
-  (#GObj.widget as 'obj) -> ('a -> unit) -> unit
+  < connect : #GObj.widget_signals ; .. > -> ('a -> unit) -> unit
 
 val use_default_doc_url : string
-- 
cgit v1.2.3


From ab276ee0e26c52e9ee049077e95e2454b17da203 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 15:45:05 +0100
Subject: CoqIDE: wm_name and wm_class are now packed into wmclass.

---
 ide/coqide.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0acbef1ad7..4b08a8795c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -359,7 +359,7 @@ let print sn =
         Filename.quote (Filename.basename f_name) ^ " | " ^ cmd_print#get
       in
       let w = GWindow.window ~title:"Print" ~modal:true
-        ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" ()
+        ~position:`CENTER ~wmclass:("CoqIDE","CoqIDE") ()
       in
       let v = GPack.vbox ~spacing:10 ~border_width:10 ~packing:w#add ()
       in
@@ -939,7 +939,7 @@ let emit_to_focus window sgn =
 
 let build_ui () =
   let w = GWindow.window
-    ~wm_class:"CoqIde" ~wm_name:"CoqIde"
+    ~wmclass:("CoqIde","CoqIde")
     ~width:window_width#get ~height:window_height#get
     ~title:"CoqIde" ()
   in
-- 
cgit v1.2.3


From 390e8b97482a3100e8d37e2e62a345f9267960e2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 15:45:46 +0100
Subject: CoqIDE: Stippling using bitmap no more supported for incomplete Qed.

Was formerly displaying a stippled ("pointillé") light blue. Now only
a light blue.
---
 ide/coqide.ml | 5 -----
 ide/tags.ml   | 2 +-
 2 files changed, 1 insertion(+), 6 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 4b08a8795c..386bd8047c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1303,11 +1303,6 @@ let build_ui () =
   let _ = source_style#connect#changed ~callback:refresh_style in
   let _ = source_language#connect#changed ~callback:refresh_language in
 
-  (* Color configuration *)
-  Tags.Script.incomplete#set_property
-    (`BACKGROUND_STIPPLE
-      (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
-
   (* Showtime ! *)
   w#show ();
   w
diff --git a/ide/tags.ml b/ide/tags.ml
index 60195e8acb..e919a64278 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -24,7 +24,7 @@ struct
   let error_bg = make_tag table ~name:"error_bg" []
   let to_process = make_tag table ~name:"to_process" []
   let processed = make_tag table ~name:"processed" []
-  let incomplete = make_tag table ~name:"incomplete" [`BACKGROUND_STIPPLE_SET true]
+  let incomplete = make_tag table ~name:"incomplete" []
   let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"]
   let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *)
   let ephemere =
-- 
cgit v1.2.3


From 153b68664adb03dde1325bdb77fa371d5aa8ff7e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 15:47:12 +0100
Subject: CoqIDE: No more explicit activation of tooltips on toolbar.

According to
https://developer.gnome.org/gtk2/stable/GtkToolbar.html#gtk-toolbar-set-tooltips,
tooltips are now managed globally by gtk-enable-tooltips which is true by default.
---
 ide/coqide.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 386bd8047c..e977ec5320 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1220,7 +1220,7 @@ let build_ui () =
       ((Coqide_ui.ui_m#get_widget "/CoqIde ToolBar")#as_widget)
   in
   let () = GtkButton.Toolbar.set
-    ~orientation:`HORIZONTAL ~style:`ICONS ~tooltips:true tbar
+    ~orientation:`HORIZONTAL ~style:`ICONS tbar
   in
   let toolbar = new GButton.toolbar tbar in
   let () = vbox#pack toolbar#coerce in
-- 
cgit v1.2.3


From d0054c9d632e13b631697523239af27d3f7ae7b4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 16:00:53 +0100
Subject: CoqIDE: Replacing deprecated color_of_string with color_parse.

---
 ide/preferences.ml | 10 +++++-----
 ide/tags.ml        | 10 ----------
 ide/tags.mli       |  3 ---
 ide/wg_Command.ml  |  2 +-
 4 files changed, 6 insertions(+), 19 deletions(-)

diff --git a/ide/preferences.ml b/ide/preferences.ml
index ee274b7001..11e27c3570 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -575,7 +575,7 @@ object (self)
     | None -> set#set_active true
     | Some c ->
       set#set_active false;
-      but#set_color (Tags.color_of_string c)
+      but#set_color (Gdk.Color.color_parse c)
     in
     track tag.tag_bg_color bg_color bg_unset;
     track tag.tag_fg_color fg_color fg_unset;
@@ -587,7 +587,7 @@ object (self)
   method tag =
     let get but set =
       if set#active then None
-      else Some (Tags.string_of_color but#color)
+      else Some (Gdk.Color.color_to_string but#color)
     in
     {
       tag_bg_color = get bg_color bg_unset;
@@ -707,15 +707,15 @@ let configure ?(apply=(fun () -> ())) parent =
       in
       let () = label#set_xalign 0. in
       let button = GButton.color_button
-        ~color:(Tags.color_of_string pref#get)
+        ~color:(Gdk.Color.color_parse pref#get)
         ~packing:(table#attach ~left:1 ~top:i) ()
       in
       let _ = button#connect#color_set ~callback:begin fun () ->
-        pref#set (Tags.string_of_color button#color)
+        pref#set (Gdk.Color.color_to_string button#color)
       end in
       let reset _ =
         pref#reset ();
-        button#set_color Tags.(color_of_string pref#get)
+        button#set_color (Gdk.Color.color_parse pref#get)
       in
       let _ = reset_button#connect#clicked ~callback:reset in
       ()
diff --git a/ide/tags.ml b/ide/tags.ml
index e919a64278..e9dbcb9e67 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -48,13 +48,3 @@ struct
   let warning = make_tag table ~name:"warning" [`FOREGROUND "orange"]
   let item = make_tag table ~name:"item" [`WEIGHT `BOLD]
 end
-
-let string_of_color clr =
-  let r = Gdk.Color.red clr in
-  let g = Gdk.Color.green clr in
-  let b = Gdk.Color.blue clr in
-  Printf.sprintf "#%04X%04X%04X" r g b
-
-let color_of_string s =
-  let colormap = Gdk.Color.get_system_colormap () in
-  Gdk.Color.alloc ~colormap (`NAME s)
diff --git a/ide/tags.mli b/ide/tags.mli
index 3194f87971..1df934fddf 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -41,6 +41,3 @@ sig
   val warning : GText.tag
   val item : GText.tag
 end
-
-val string_of_color : Gdk.color -> string
-val color_of_string : string -> Gdk.color
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 06281d6287..57e467f5dd 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -163,7 +163,7 @@ object(self)
     frame#visible
 
   method private refresh_color clr =
-    let clr = Tags.color_of_string clr in
+    let clr = Gdk.Color.color_parse clr in
     let iter (_,view,_) = view#misc#modify_base [`NORMAL, `COLOR clr] in
     List.iter iter views
 
-- 
cgit v1.2.3


From ae3fa5305a034015a894e3fa6f6cea27c4138b9a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 21 Nov 2018 23:48:25 +0100
Subject: CoqIDE: Adapting to new interface of GPack.notebook.

---
 ide/wg_Notebook.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/ide/wg_Notebook.mli b/ide/wg_Notebook.mli
index 85ecdf6cdd..9447b21c0b 100644
--- a/ide/wg_Notebook.mli
+++ b/ide/wg_Notebook.mli
@@ -28,11 +28,10 @@ val create :
   ('a -> GObj.widget option * GObj.widget option * GObj.widget) ->
   ('a -> unit) ->
   ?enable_popup:bool ->
-  ?homogeneous_tabs:bool ->
+  ?group_name:string ->
   ?scrollable:bool ->
   ?show_border:bool ->
   ?show_tabs:bool ->
-  ?tab_border:int ->
   ?tab_pos:Gtk.Tags.position ->
   ?border_width:int ->
   ?width:int ->
-- 
cgit v1.2.3


From 0f91d7fbbaf790e84b30f60410ddae4cbbd9c3eb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 01:02:59 +0100
Subject: CoqIDE: Using Grid instead of Table.

This is not mandatory for gtk+3 since it is deprecated from only gtk
3.4. This would be needed for gtk+4 though.
---
 ide/preferences.ml | 12 ++++++------
 ide/wg_Find.ml     | 20 ++++++++++----------
 2 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 11e27c3570..cf884b7107 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -691,7 +691,7 @@ let configure ?(apply=(fun () -> ())) parent =
 
   let config_color =
     let box = GPack.vbox () in
-    let table = GPack.table
+    let grid = GPack.grid
       ~row_spacings:5
       ~col_spacings:5
       ~border_width:2
@@ -703,12 +703,12 @@ let configure ?(apply=(fun () -> ())) parent =
     in
     let iter i (text, pref) =
       let label = GMisc.label
-        ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:i) ()
+        ~text ~packing:(grid#attach (*~expand:`X*) ~left:0 ~top:i) ()
       in
       let () = label#set_xalign 0. in
       let button = GButton.color_button
         ~color:(Gdk.Color.color_parse pref#get)
-        ~packing:(table#attach ~left:1 ~top:i) ()
+        ~packing:(grid#attach ~left:1 ~top:i) ()
       in
       let _ = button#connect#color_set ~callback:begin fun () ->
         pref#set (Gdk.Color.color_to_string button#color)
@@ -740,7 +740,7 @@ let configure ?(apply=(fun () -> ())) parent =
       ~packing:(box#pack ~expand:true)
       ()
     in
-    let table = GPack.table
+    let grid = GPack.grid
       ~row_spacings:5
       ~col_spacings:5
       ~border_width:2
@@ -750,13 +750,13 @@ let configure ?(apply=(fun () -> ())) parent =
     let cb = ref [] in
     let iter text tag =
       let label = GMisc.label
-        ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:!i) ()
+        ~text ~packing:(grid#attach (*~expand:`X*) ~left:0 ~top:!i) ()
       in
       let () = label#set_xalign 0. in
       let button = tag_button () in
       let callback () = tag#set button#tag in
       button#set_tag tag#get;
-      table#attach ~left:1 ~top:!i button#coerce;
+      grid#attach ~left:1 ~top:!i button#coerce;
       incr i;
       cb := callback :: !cb;
     in
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 7d2d7da570..448eeadad8 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -14,10 +14,10 @@ class finder name (view : GText.view) =
   
   let widget = Wg_Detachable.detachable
     ~title:(Printf.sprintf "Find & Replace (%s)" name) () in 
-  let replace_box = GPack.table ~columns:4 ~rows:2 ~homogeneous:false
+  let replace_box = GPack.grid (* ~columns:4 ~rows:2 *) ~col_homogeneous:false ~row_homogeneous:false
     ~packing:widget#add () in
   let hb = GPack.hbox ~packing:(replace_box#attach
-      ~left:1 ~top:0 ~expand:`X ~fill:`X) () in
+      ~left:1 ~top:0 (*~expand:`X ~fill:`X*)) () in
   let use_regex =
     GButton.check_button ~label:"Regular expression"
       ~packing:(hb#pack ~expand:false ~fill:true ~padding:3) () in
@@ -26,25 +26,25 @@ class finder name (view : GText.view) =
       ~packing:(hb#pack ~expand:false ~fill:true ~padding:3) () in
   let _ = GMisc.label ~text:"Find:" ~xalign:1.0
     ~packing:(replace_box#attach
-      ~xpadding:3 ~ypadding:3 ~left:0 ~top:1 ~fill:`X) () in
+     (*~xpadding:3 ~ypadding:3*) ~left:0 ~top:1 (*~fill:`X*)) () in
   let _ = GMisc.label ~text:"Replace:" ~xalign:1.0
     ~packing:(replace_box#attach
-      ~xpadding:3 ~ypadding:3 ~left:0 ~top:2 ~fill:`X) () in
+     (* ~xpadding:3 ~ypadding:3*) ~left:0 ~top:2 (*~fill:`X*)) () in
   let find_entry = GEdit.entry ~editable:true
     ~packing:(replace_box#attach
-      ~xpadding:3 ~ypadding:3 ~left:1 ~top:1 ~expand:`X ~fill:`X) () in
+      (*~xpadding:3 ~ypadding:3*) ~left:1 ~top:1 (*~expand:`X ~fill:`X*)) () in
   let replace_entry = GEdit.entry ~editable:true
     ~packing:(replace_box#attach
-      ~xpadding:3 ~ypadding:3 ~left:1 ~top:2 ~expand:`X ~fill:`X) () in
+      (*~xpadding:3 ~ypadding:3*) ~left:1 ~top:2 (*~expand:`X ~fill:`X*)) () in
   let next_button = GButton.button ~label:"_Next" ~use_mnemonic:true
-    ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:2 ~top:1) () in
+    ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:2 ~top:1) () in
   let previous_button = GButton.button ~label:"_Previous" ~use_mnemonic:true
-    ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:3 ~top:1) () in
+    ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:3 ~top:1) () in
   let replace_button = GButton.button ~label:"_Replace" ~use_mnemonic:true
-    ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:2 ~top:2) () in
+    ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:2 ~top:2) () in
   let replace_all_button =
     GButton.button ~label:"Replace _All" ~use_mnemonic:true
-      ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:3 ~top:2) () in
+      ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:3 ~top:2) () in
 
   object (self)
     val mutable last_found = None
-- 
cgit v1.2.3


From 1e6dd0a21569f32a8046bb29400928ef3a6a1fa1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Nov 2018 03:18:57 +0100
Subject: CoqIDE: Ensure that contents of the pref window expands as much as
 possible.

This was not needed in gtk2 but is needed with gtk3.
---
 ide/configwin_ihm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml
index 9fe3d8bb35..0f3fd38a7a 100644
--- a/ide/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
@@ -660,7 +660,7 @@ let edit ?(with_apply=true)
   in
   let config_box = new configuration_box conf_struct in
 
-  let _ = dialog#vbox#add config_box#box#coerce in
+  let _ = dialog#vbox#pack ~expand:true config_box#box#coerce in
 
   if with_apply then
     dialog#add_button Configwin_messages.mApply `APPLY;
-- 
cgit v1.2.3


From a68bc1f4211f089f6030bf44d3f5df88db170c18 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Nov 2018 03:47:26 +0100
Subject: CoqIDE: Ensure that the main 3 windows do not shrink when w/o
 contents.

This was automatic in gtk2 (apparently because of the specification
not being granted). This is needed with gtk3.
---
 ide/session.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/ide/session.ml b/ide/session.ml
index b7f98f3d79..22aaef399d 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -442,11 +442,11 @@ let build_layout (sn:session) =
   let eval_paned = GPack.paned `HORIZONTAL ~border_width:5
     ~packing:(session_box#pack ~expand:true) () in
   let script_frame = GBin.frame ~shadow_type:`IN
-    ~packing:eval_paned#add1 () in
+    ~packing:(eval_paned#pack1 ~shrink:false) () in
   let script_scroll = GBin.scrolled_window
     ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:script_frame#add () in
   let state_paned = GPack.paned `VERTICAL
-    ~packing:eval_paned#add2 () in
+    ~packing:(eval_paned#pack2 ~shrink:false) () in
 
   (* Proof buffer. *)
 
-- 
cgit v1.2.3


From b373967afc2ba95fdeb850c1af9c89637a2afbb4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Nov 2018 15:37:14 +0100
Subject: CoqIDE: Use modify_bg rather than modify_base to change background
 color.

The effect of modify_base is told to be widget-dependent. It uses to
change the background with gtk2 but not with gtk3. So we use the more
explicit modify_bg.
---
 ide/session.ml        | 2 +-
 ide/wg_Command.ml     | 4 ++--
 ide/wg_Find.ml        | 6 +++---
 ide/wg_MessageView.ml | 2 +-
 ide/wg_ProofView.ml   | 2 +-
 ide/wg_ScriptView.ml  | 2 +-
 6 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/ide/session.ml b/ide/session.ml
index 22aaef399d..fd21515ca5 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -257,7 +257,7 @@ let make_table_widget ?sort cd cb =
       ~model:store ~packing:frame#add () in
   let () = data#set_headers_visible true in
   let () = data#set_headers_clickable true in
-  let refresh clr = data#misc#modify_base [`NORMAL, `NAME clr] in
+  let refresh clr = data#misc#modify_bg [`NORMAL, `NAME clr] in
   let _ = background_color#connect#changed ~callback:refresh in
   let _ = data#misc#connect#realize ~callback:(fun () -> refresh background_color#get) in
   let mk_rend c = GTree.cell_renderer_text [], ["text",c] in
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 57e467f5dd..dce2a0726b 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -100,7 +100,7 @@ object(self)
     router#register_route route_id result;
     r_bin#add_with_viewport (result :> GObj.widget);
     views <- (frame#coerce, result, combo#entry) :: views;
-    let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in
+    let cb clr = result#misc#modify_bg [`NORMAL, `NAME clr] in
     let _ = background_color#connect#changed ~callback:cb in
     let _ = result#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
     let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in
@@ -164,7 +164,7 @@ object(self)
 
   method private refresh_color clr =
     let clr = Gdk.Color.color_parse clr in
-    let iter (_,view,_) = view#misc#modify_base [`NORMAL, `COLOR clr] in
+    let iter (_,view,_) = view#misc#modify_bg [`NORMAL, `COLOR clr] in
     List.iter iter views
 
   initializer
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 448eeadad8..fe079e8a9e 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -135,13 +135,13 @@ class finder name (view : GText.view) =
       view#buffer#end_user_action ()
 
     method private set_not_found () =
-      find_entry#misc#modify_base [`NORMAL, `NAME "#F7E6E6"];
+      find_entry#misc#modify_bg [`NORMAL, `NAME "#F7E6E6"];
 
     method private set_found () =
-      find_entry#misc#modify_base [`NORMAL, `NAME "#BAF9CE"]
+      find_entry#misc#modify_bg [`NORMAL, `NAME "#BAF9CE"]
 
     method private set_normal () =
-      find_entry#misc#modify_base [`NORMAL, `NAME "white"]
+      find_entry#misc#modify_bg [`NORMAL, `NAME "white"]
 
     method private find_from backward ?(wrapped=false) (starti : GText.iter) =
       let found =
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index b302cbc066..fd69d5e623 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -59,7 +59,7 @@ let message_view () : message_view =
   let _ = buffer#add_selection_clipboard default_clipboard in
   let () = view#set_left_margin 2 in
   view#misc#show ();
-  let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
+  let cb clr = view#misc#modify_bg [`NORMAL, `NAME clr] in
   let _ = background_color#connect#changed ~callback:cb in
   let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
   let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 7894ded532..beeba4ade6 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -204,7 +204,7 @@ let proof_view () =
   let () = Gtk_parsing.fix_double_click view in
   let default_clipboard = GData.clipboard Gdk.Atom.primary in
   let _ = buffer#add_selection_clipboard default_clipboard in
-  let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
+  let cb clr = view#misc#modify_bg [`NORMAL, `NAME clr] in
   let _ = background_color#connect#changed ~callback:cb in
   let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
   let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 8677f5fc65..7812f1a222 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -461,7 +461,7 @@ object (self)
     in
     let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in
     (* Plug on preferences *)
-    let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in
+    let cb clr = self#misc#modify_bg [`NORMAL, `NAME clr] in
     let _ = background_color#connect#changed ~callback:cb in
     let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
 
-- 
cgit v1.2.3


From 7af4cbfda15a8bb3300aeae7e074c7527cc7af10 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 23 Dec 2018 19:55:09 +0100
Subject: CoqIDE: Ensuring that load/save windows are not hidden by their
 parent.

---
 ide/coqide.ml    | 8 ++++----
 ide/ideutils.ml  | 8 ++++----
 ide/ideutils.mli | 5 +++--
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index e977ec5320..2f2478372e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -193,7 +193,7 @@ let confirm_save ok =
 let select_and_save ?parent ~saveas ?filename sn =
   let do_save = if saveas then sn.fileops#saveas ?parent else sn.fileops#save in
   let title = if saveas then "Save file as" else "Save file" in
-  match select_file_for_save ~title ?filename () with
+  match select_file_for_save ~title ?parent ?filename () with
     |None -> false
     |Some f ->
       let ok = do_save f in
@@ -271,11 +271,11 @@ let newfile _ =
   let index = notebook#append_term session in
   notebook#goto_page index
 
-let load _ =
+let load ?parent _ =
   let filename =
     try notebook#current_term.fileops#filename
     with Invalid_argument _ -> None in
-  match select_file_for_open ~title:"Load file" ?filename () with
+  match select_file_for_open ~title:"Load file" ?parent ?filename () with
     | None -> ()
     | Some f -> FileAux.load_file f
 
@@ -972,7 +972,7 @@ let build_ui () =
   menu file_menu [
     item "File" ~label:"_File";
     item "New" ~callback:File.newfile ~stock:`NEW;
-    item "Open" ~callback:File.load ~stock:`OPEN;
+    item "Open" ~callback:(File.load ~parent:w) ~stock:`OPEN;
     item "Save" ~callback:(File.save ~parent:w) ~stock:`SAVE ~tooltip:"Save current buffer";
     item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:(File.saveas ~parent:w);
     item "Save all" ~label:"Sa_ve all" ~callback:File.saveall;
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index d0fbf796a0..8c5b3fcc5b 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -230,9 +230,9 @@ let current_dir () = match project_path#get with
 | None -> ""
 | Some dir -> dir
 
-let select_file_for_open ~title ?(filter=true) ?filename () =
+let select_file_for_open ~title ?(filter=true) ?parent ?filename () =
   let file_chooser =
-    GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title ()
+    GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title ?parent ()
   in
   file_chooser#add_button_stock `CANCEL `CANCEL ;
   file_chooser#add_select_button_stock `OPEN `OPEN ;
@@ -259,10 +259,10 @@ let select_file_for_open ~title ?(filter=true) ?filename () =
   file_chooser#destroy ();
   file
 
-let select_file_for_save ~title ?filename () =
+let select_file_for_save ~title ?parent ?filename () =
   let file = ref None in
   let file_chooser =
-    GWindow.file_chooser_dialog ~action:`SAVE ~modal:true ~title ()
+    GWindow.file_chooser_dialog ~action:`SAVE ~modal:true ~title ?parent ()
   in
   file_chooser#add_button_stock `CANCEL `CANCEL ;
   file_chooser#add_select_button_stock `SAVE `SAVE ;
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index cc7d865325..57f59d19fe 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -30,9 +30,10 @@ val find_tag_limits : GText.tag -> GText.iter -> GText.iter * GText.iter
 val find_tag_start : GText.tag -> GText.iter -> GText.iter
 val find_tag_stop : GText.tag -> GText.iter -> GText.iter
 
-val select_file_for_open : title:string -> ?filter:bool -> ?filename:string -> unit -> string option
+val select_file_for_open :
+  title:string -> ?filter:bool -> ?parent:GWindow.window -> ?filename:string -> unit -> string option
 val select_file_for_save :
-  title:string -> ?filename:string -> unit -> string option
+  title:string -> ?parent:GWindow.window -> ?filename:string -> unit -> string option
 val try_convert : string -> string
 val try_export : string -> string -> bool
 val stock_to_widget :
-- 
cgit v1.2.3


From 68c1261978639a6a8e8467294fb6eaf3d70a2234 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 23 Dec 2018 20:37:22 +0100
Subject: CoqIDE: Advertising gtk+3 upgrade in CHANGES.

---
 CHANGES.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 3e50a13e9e..1e64b78d2e 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -17,6 +17,8 @@ OCaml and dependencies
 
 Coqide
 
+- CoqIDE now depends on gtk+3 and lablgtk3, rather than gtk+2 and lablgtk2.
+
 - CoqIDE now properly sets the module name for a given file based on
   its path, see -topfile change entry for more details.
 
-- 
cgit v1.2.3


From 25cbf4cefa2102b11c3617c0c52f67d98fbffaac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 6 Jan 2019 19:40:04 +0100
Subject: CoqIDE: More informative message when failing editing/saving
 preferences.

---
 ide/coqide.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2f2478372e..49ff53eda1 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -213,7 +213,8 @@ let check_save ?parent ~saveas sn =
 exception DontQuit
 
 let check_quit ?parent saveall =
-  (try save_pref () with _ -> flash_info "Cannot save preferences");
+  (try save_pref ()
+   with e -> flash_info ("Cannot save preferences (" ^ Printexc.to_string e ^ ")"));
   let is_modified sn = sn.buffer#modified in
   if List.exists is_modified notebook#pages then begin
     let answ = Configwin_ihm.question_box ~title:"Quit"
@@ -1021,7 +1022,8 @@ let build_ui () =
       ~callback:(fun _ ->
         begin
 	  try Preferences.configure ~apply:refresh_notebook_pos w
-	  with _ -> flash_info "Cannot save preferences"
+          with e ->
+            flash_info ("Editing preferences failed (" ^ Printexc.to_string e ^ ")")
         end;
         reset_revert_timer ());
   ];
-- 
cgit v1.2.3


From 73847d367b22b5d451bcf1e538b80ca057232754 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 6 Jan 2019 19:40:30 +0100
Subject: CoqIDE: Adding configurable color for incompletely processed Qed.

---
 ide/preferences.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/ide/preferences.ml b/ide/preferences.ml
index cf884b7107..69dbc0b235 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -413,8 +413,11 @@ let attach_fg (pref : string preference) (tag : GText.tag) =
 let processing_color =
   new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string)
 
+let incompletely_processed_color =
+  new preference ~name:["incompletely_processed_color"] ~init:"light sky blue" ~repr:Repr.(string)
+
 let _ = attach_bg processing_color Tags.Script.to_process
-let _ = attach_bg processing_color Tags.Script.incomplete
+let _ = attach_bg incompletely_processed_color Tags.Script.incomplete
 
 let tags = ref Util.String.Map.empty
 
@@ -724,6 +727,7 @@ let configure ?(apply=(fun () -> ())) parent =
       ("Background color", background_color);
       ("Background color of processed text", processed_color);
       ("Background color of text being processed", processing_color);
+      ("Background color of incompletely processed Qed", incompletely_processed_color);
       ("Background color of errors", error_color);
       ("Foreground color of errors", error_fg_color);
     ] in
-- 
cgit v1.2.3


From 4d69a22ffa06005b11040c9db9064a1d730eeb7f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 7 Feb 2019 16:54:11 +0100
Subject: Fix for post-beta3 lablgtk3 changes about cairo (from Claudio).

---
 ide/coqide.ml         | 2 +-
 ide/wg_Command.ml     | 2 +-
 ide/wg_MessageView.ml | 2 +-
 ide/wg_ProofView.ml   | 2 +-
 ide/wg_ScriptView.ml  | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 49ff53eda1..eaeeaa0001 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -813,7 +813,7 @@ let zoom_fit sn =
   let space = script#misc#allocation.Gtk.width in
   let cols = script#right_margin_position in
   let pango_ctx = script#misc#pango_context in
-  let layout = pango_ctx#create_layout in
+  let layout = pango_ctx#create_layout#as_layout in
   let fsize = Pango.Font.get_size (Pango.Font.from_string text_font#get) in
   Pango.Layout.set_text layout (String.make cols 'X');
   let tlen = fst (Pango.Layout.get_pixel_size layout) in
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index dce2a0726b..be400a5f2d 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -103,7 +103,7 @@ object(self)
     let cb clr = result#misc#modify_bg [`NORMAL, `NAME clr] in
     let _ = background_color#connect#changed ~callback:cb in
     let _ = result#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
-    let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in
+    let cb ft = result#misc#modify_font (GPango.font_description_from_string ft) in
     stick text_font result cb;
     result#misc#set_can_focus true; (* false causes problems for selection *)
     let callback () =
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index fd69d5e623..7943b099fc 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -62,7 +62,7 @@ let message_view () : message_view =
   let cb clr = view#misc#modify_bg [`NORMAL, `NAME clr] in
   let _ = background_color#connect#changed ~callback:cb in
   let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
-  let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
+  let cb ft = view#misc#modify_font (GPango.font_description_from_string ft) in
   stick text_font view cb;
 
   (* Inserts at point, advances the mark *)
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index beeba4ade6..596df227b7 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -207,7 +207,7 @@ let proof_view () =
   let cb clr = view#misc#modify_bg [`NORMAL, `NAME clr] in
   let _ = background_color#connect#changed ~callback:cb in
   let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
-  let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
+  let cb ft = view#misc#modify_font (GPango.font_description_from_string ft) in
   stick text_font view cb;
 
   let pf = object
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 7812f1a222..e95176bf4d 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -484,7 +484,7 @@ object (self)
     stick tab_length self self#set_tab_width;
     stick auto_complete self self#set_auto_complete;
 
-    let cb ft = self#misc#modify_font (Pango.Font.from_string ft) in
+    let cb ft = self#misc#modify_font (GPango.font_description_from_string ft) in
     stick text_font self cb;
 
     ()
-- 
cgit v1.2.3


From e3501ed973ddf4958e309d855c4d5d762e2f6e9d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 9 Feb 2019 20:59:04 +0100
Subject: [coqide] [ci] Update GTK toolchain to lablgtk3

- Update Docker images to install compatible version of lablgtk3
- We remove unnecesary variables from configure.
- We fix path detection of GTK libs in makefile
---
 .gitlab-ci.yml                                     |   2 +-
 Makefile.ide                                       |  21 +-
 configure.ml                                       |  93 +++------
 coqide.opam                                        |   6 +-
 default.nix                                        |   5 +-
 dev/build/windows/MakeCoq_MinGW.bat                |   2 +-
 dev/build/windows/makecoq_mingw.sh                 | 204 +++++++-------------
 dev/build/windows/patches_coq/VST.patch            |   0
 dev/build/windows/patches_coq/flexdll-0.37.patch   |  19 ++
 .../windows/patches_coq/gtksourceview-2.11.2.patch | 213 ---------------------
 dev/build/windows/patches_coq/lablgtk-2.18.6.patch | 101 ----------
 .../windows/patches_coq/lablgtk-3.0.beta5.patch    |  76 ++++++++
 dev/build/windows/patches_coq/quickchick.patch     |   0
 dev/ci/docker/bionic_coq/Dockerfile                |  13 +-
 ide/dune                                           |   2 +-
 ide/ide.mllib                                      |   1 -
 ide/wg_Detachable.ml                               |   3 +
 17 files changed, 227 insertions(+), 534 deletions(-)
 mode change 100755 => 100644 dev/build/windows/patches_coq/VST.patch
 create mode 100644 dev/build/windows/patches_coq/flexdll-0.37.patch
 delete mode 100644 dev/build/windows/patches_coq/gtksourceview-2.11.2.patch
 delete mode 100644 dev/build/windows/patches_coq/lablgtk-2.18.6.patch
 create mode 100644 dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch
 mode change 100755 => 100644 dev/build/windows/patches_coq/quickchick.patch

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 309044a1e9..58bf6bf065 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -10,7 +10,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2019-03-11-V1"
+  CACHEKEY: "bionic_coq-V2019-03-12-V1"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/Makefile.ide b/Makefile.ide
index 86bdaf62d4..778863d1fc 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -17,7 +17,6 @@
 
 ## Coqide-related variables set by ./configure in config/Makefile
 
-#COQIDEINCLUDES : something like -I +lablgtk3
 #HASCOQIDE : opt / byte / no
 #IDEFLAGS : some extra cma, for instance
 #IDEOPTCDEPS : on windows, ide/ide_win32_stubs.o ide/coq_icon.o
@@ -41,7 +40,11 @@ COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
 
 IDESRCDIRS:= $(CORESRCDIRS) ide ide/protocol
 
-COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
+ifeq ($(HASCOQIDE),no)
+COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS))
+else
+COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) -package lablgtk3-sourceview3
+endif
 
 IDEDEPS:=config/config.cma clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma
 IDECMA:=ide/ide.cma
@@ -56,11 +59,11 @@ IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_
 
 ## GTK for Coqide MacOS bundle
 
-GTKSHARE=$(shell pkg-config --variable=prefix gtk+-2.0)/share
-GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin
-GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
-PIXBUFBIN=$(shell pkg-config --variable=prefix gdk-pixbuf-2.0)/bin
-SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-2.0)/share
+GTKSHARE=$(shell pkg-config --variable=prefix gtk+-3.0)/share
+GTKBIN=$(shell pkg-config --variable=prefix gtk+-3.0)/bin
+GTKLIBS=$(shell pkg-config --variable=libdir gtk+-3.0)
+PIXBUFBIN=$(shell pkg-config --variable=prefix gdk-pixbuf-3.0)/bin
+SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-3.0)/share
 
 ###########################################################################
 # CoqIde special targets
@@ -98,7 +101,7 @@ ifeq ($(HASCOQIDE),opt)
 $(COQIDE): $(LINKIDEOPT)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
-	       -linkpkg -package str,unix,dynlink,threads,lablgtk3.sourceview3 $(IDEFLAGS:.cma=.cmxa) $^
+	       -linkpkg -package str,unix,dynlink,threads,lablgtk3-sourceview3 -linkall $(IDEFLAGS:.cma=.cmxa) $^
 	$(STRIP_HIDE) $@
 else
 $(COQIDE): $(COQIDEBYTE)
@@ -108,7 +111,7 @@ endif
 $(COQIDEBYTE): $(LINKIDE)
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \
-	       -linkpkg -package str,unix,dynlink,threads,lablgtk3.sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
+	       -linkpkg -package str,unix,dynlink,threads,lablgtk3-sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
 
 ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile
 	@rm -f $@
diff --git a/configure.ml b/configure.ml
index 14698c4e61..5b99851f83 100644
--- a/configure.ml
+++ b/configure.ml
@@ -153,6 +153,7 @@ let numeric_prefix_list s =
   match string_split '.' (String.sub s 0 !i) with
   | [v] -> [v;"0";"0"]
   | [v1;v2] -> [v1;v2;"0"]
+  | [v1;v2;""] -> [v1;v2;"0"] (* e.g. because it ends with ".beta" *)
   | v -> v
 
 (** Combined existence and directory tests *)
@@ -229,7 +230,6 @@ type preferences = {
   docdir : string option;
   coqdocdir : string option;
   ocamlfindcmd : string option;
-  lablgtkdir : string option;
   arch : string option;
   natdynlink : bool;
   coqide : ide option;
@@ -266,7 +266,6 @@ let default = {
   docdir = None;
   coqdocdir = None;
   ocamlfindcmd = None;
-  lablgtkdir = None;
   arch = None;
   natdynlink = true;
   coqide = None;
@@ -371,8 +370,6 @@ let args_options = Arg.align [
     "<dir> Where to install Coqdoc style files";
   "-ocamlfind", arg_string_option (fun p ocamlfindcmd -> { p with ocamlfindcmd }),
     "<dir> Specifies the ocamlfind command to use";
-  "-lablgtkdir", arg_string_option (fun p lablgtkdir -> { p with lablgtkdir }),
-    "<dir> Specifies the path to the Lablgtk library";
   "-flambda-opts", arg_string_list ' ' (fun p flambda_flags -> { p with flambda_flags }),
     "<flags> Specifies additional flags to be passed to the flambda optimizing compiler";
   "-arch", arg_string_option (fun p arch -> { p with arch }),
@@ -702,63 +699,29 @@ let numlib =
 
 (** * lablgtk3 and CoqIDE *)
 
-type source = Manual | OCamlFind | Stdlib
-
-let get_source = function
-| Manual -> "manually provided"
-| OCamlFind -> "via ocamlfind"
-| Stdlib -> "in OCaml library"
-
-(** Is some location a suitable LablGtk2 installation ? *)
-
-let check_lablgtkdir ?(fatal=false) src dir =
-  let yell msg = if fatal then die msg else (warn "%s" msg; false) in
-  let msg = get_source src in
-  if not (dir_exists dir) then
-    yell (sprintf "No such directory '%s' (%s)." dir msg)
-  else if not (Sys.file_exists (dir/"gSourceView2.cmi") || Sys.file_exists (dir/"gSourceView3.cmi")) then
-    yell (sprintf "Incomplete LablGtk2 (%s): no %s/gSourceView2.cmi." msg dir)
-  else if not (Sys.file_exists (dir/"glib.mli")) then
-    yell (sprintf "Incomplete LablGtk2 (%s): no %s/glib.mli." msg dir)
-  else true
-
-(** Detect and/or verify the Lablgtk2 location *)
+(** Detect and/or verify the Lablgtk3 location *)
 
 let get_lablgtkdir () =
-  match !prefs.lablgtkdir with
-  | Some dir ->
-    let msg = Manual in
-    if check_lablgtkdir ~fatal:true msg dir then dir, msg
-    else "", msg
-  | None ->
-    let msg = OCamlFind in
-    let d1,_ = tryrun camlexec.find ["query";"lablgtk3.sourceview3"] in
-    if d1 <> "" && check_lablgtkdir msg d1 then d1, msg
-    else
-      (* In debian wheezy, ocamlfind knows only of lablgtk3 *)
-      let d2,_ = tryrun camlexec.find ["query";"lablgtk3"] in
-      if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg
-      else
-        let msg = Stdlib in
-        let d3 = camllib^"/lablgtk3" in
-        if check_lablgtkdir msg d3 then d3, msg
-        else "", msg
+  tryrun camlexec.find ["query";"lablgtk3-sourceview3"]
 
 (** Detect and/or verify the Lablgtk2 version *)
 
-let check_lablgtk_version src dir = match src with
-| Manual | Stdlib ->
-  warn "Could not check the version of lablgtk3.\nMake sure your version is at least 3.0.0.";
-  (true, "an unknown version")
-| OCamlFind ->
+let check_lablgtk_version () =
   let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk3"] in
-  try
-    let vi = List.map s2i (numeric_prefix_list v) in
+  (true, v)
+
+(* ejgallego: we wait to do version checks until an official release is out *)
+(*  try
+    let vi = numeric_prefix_list v in
+    (* Temporary hack *)
+    if vi = ["3";"0";"beta3"] then (false, v) else
+    let vi = List.map s2i vi in
     if vi < [3; 0; 0] then
       (false, v)
     else
       (true, v)
   with _ -> (false, v)
+*)
 
 let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native"
 
@@ -781,19 +744,19 @@ let lablgtkdir = ref ""
 let check_coqide () =
   if !prefs.coqide = Some No then set_ide No "CoqIde manually disabled";
   let dir, via = get_lablgtkdir () in
-  if dir = "" then set_ide No "LablGtk3 not found";
-  let (ok, version) = check_lablgtk_version via dir in
-  let found = sprintf "LablGtk3 found (%s, %s)" (get_source via) version in
-  if not ok then set_ide No (found^", but too old (required >= 3.0, found " ^ version ^ ")");
-  (* We're now sure to produce at least one kind of coqide *)
-  lablgtkdir := shorten_camllib dir;
-  if !prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested");
-  if best_compiler<>"opt" then set_ide Byte (found^", but no native compiler");
-  if not (Sys.file_exists (dir/"gtkThread.cmx")) then
-    set_ide Byte (found^", but no native LablGtk2");
-  if not (Sys.file_exists (camllib/"threads"/"threads.cmxa")) then
-    set_ide Byte (found^", but no native threads");
-  set_ide Opt (found^", with native threads")
+  if dir = ""
+  then set_ide No "LablGtk3 not found"
+  else
+    let (ok, version) = check_lablgtk_version () in
+    let found = sprintf "LablGtk3 found (%s)" version in
+    if not ok then set_ide No (found^", but too old (required >= 3.0, found " ^ version ^ ")");
+    (* We're now sure to produce at least one kind of coqide *)
+    lablgtkdir := shorten_camllib dir;
+    if !prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested");
+    if best_compiler <> "opt" then set_ide Byte (found^", but no native compiler");
+    if not (Sys.file_exists (camllib/"threads"/"threads.cmxa")) then
+      set_ide Byte (found^", but no native threads");
+    set_ide Opt (found^", with native threads")
 
 let coqide =
   try check_coqide ()
@@ -801,19 +764,16 @@ let coqide =
 
 (** System-specific CoqIde flags *)
 
-let lablgtkincludes = ref ""
 let idearchflags = ref ""
 let idearchfile = ref ""
 let idecdepsflags = ref ""
 let idearchdef = ref "X11"
 
 let coqide_flags () =
-  if !lablgtkdir <> "" then lablgtkincludes := sprintf "-I %S" !lablgtkdir;
   match coqide, arch with
     | "opt", "Darwin" when !prefs.macintegration ->
       let osxdir,_ = tryrun camlexec.find ["query";"lablgtkosx"] in
       if osxdir <> "" then begin
-        lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir;
         idearchflags := "lablgtkosx.cma";
         idearchdef := "QUARTZ"
       end
@@ -1196,7 +1156,6 @@ let write_makefile f =
   pr "# Unix systems and no profiling: strip\n";
   pr "STRIP=%s\n\n" strip;
   pr "# LablGTK\n";
-  pr "COQIDEINCLUDES=%s\n\n" !lablgtkincludes;
   pr "# CoqIde (no/byte/opt)\n";
   pr "HASCOQIDE=%s\n" coqide;
   pr "IDEFLAGS=%s\n" !idearchflags;
diff --git a/coqide.opam b/coqide.opam
index 9e22091898..c82fa72564 100644
--- a/coqide.opam
+++ b/coqide.opam
@@ -17,10 +17,10 @@ dev-repo: "git+https://github.com/coq/coq.git"
 license: "LGPL-2.1"
 
 depends: [
-  "dune"               { build & >= "1.4.0" }
+  "dune"                 { build & >= "1.4.0" }
   "coqide-server"
-  "conf-gtksourceview3"
-  "lablgtk3"
+  "lablgtk3"             {         >= "3.0.beta5" }
+  "lablgtk3-sourceview3" {         >= "3.0.beta5" }
 ]
 
 build-env: [
diff --git a/default.nix b/default.nix
index cede0cd6b1..3cc0bfb11f 100644
--- a/default.nix
+++ b/default.nix
@@ -45,7 +45,10 @@ stdenv.mkDerivation rec {
     dune
   ]
   ++ (with ocamlPackages; [ ocaml findlib num ])
-  ++ optional buildIde ocamlPackages.lablgtk
+  ++ optionals buildIde [
+    ocamlPackages.lablgtk3-sourceview3
+    glib gnome3.defaultIconTheme wrapGAppsHook
+  ]
   ++ optionals buildDoc [
     # Sphinx doc dependencies
     pkgconfig (python3.withPackages
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index c8cfcf60c8..c3f3a97ff5 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -331,7 +331,7 @@ IF "%CYGWIN_QUIET%" == "Y" (
 )
 
 IF "%GTK_FROM_SOURCES%"=="N" (
-  SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
+  SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk3,mingw64-%ARCH%-gtksourceview3.0
 )
 
 REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 43f44a80b4..03bda8d0c0 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -742,7 +742,7 @@ function make_fontconfig {
 ##### ICONV #####
 
 function make_libiconv {
-  build_conf_make_inst  http://ftp.gnu.org/pub/gnu/libiconv  libiconv-1.14  tar.gz  true
+  build_conf_make_inst  http://ftp.gnu.org/pub/gnu/libiconv  libiconv-1.15  tar.gz  true
 }
 
 ##### UNISTRING #####
@@ -816,7 +816,9 @@ function make_glib {
   make_gettext
   make_libffi
   make_libpcre
+
   build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/glib/2.57  glib-2.57.1  tar.xz  true
+
 }
 
 ##### ATK #####
@@ -824,7 +826,7 @@ function make_glib {
 function make_atk {
   make_gettext
   make_glib
-  build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/atk/2.29  atk-2.29.1  tar.xz  true
+  build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/atk/2.30  atk-2.30.0  tar.xz  true
 }
 
 ##### PIXBUF #####
@@ -837,7 +839,7 @@ function make_gdk-pixbuf {
   # CONFIGURE PARAMETERS
   # --with-included-loaders=yes statically links the image file format handlers
   # This avoids "Cannot open pixbuf loader module file '/usr/x86_64-w64-mingw32/sys-root/mingw/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache': No such file or directory"
-  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.36  gdk-pixbuf-2.36.12  tar.xz  true  --with-included-loaders=yes
+  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.38  gdk-pixbuf-2.38.0  tar.xz  true  --with-included-loaders=yes
 }
 
 ##### CAIRO #####
@@ -848,7 +850,7 @@ function make_cairo {
   make_glib
   make_pixman
   make_fontconfig
-  build_conf_make_inst  http://cairographics.org/releases  rcairo-1.15.13  tar.xz  true
+  build_conf_make_inst  http://cairographics.org/releases  rcairo-1.16.2  tar.xz  true
 }
 
 ##### PANGO #####
@@ -857,37 +859,23 @@ function make_pango {
   make_cairo
   make_glib
   make_fontconfig
-  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/pango/1.42  pango-1.42.1  tar.xz  true
+  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/pango/1.42  pango-1.42.4  tar.xz  true
 }
 
-##### GTK2 #####
+##### GTK3 #####
 
-function patch_gtk2 {
-  rm gtk/gtk.def
-}
+function make_gtk3 {
 
-function make_gtk2 {
-  # Cygwin packet dependencies: gtk-update-icon-cache
   if [ "$GTK_FROM_SOURCES" == "Y" ]; then
-    make_glib
-    make_atk
-    make_pango
-    make_gdk-pixbuf
-    make_cairo
-    build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/gtk+/2.24  gtk+-2.24.32  tar.xz  patch_gtk2
-  fi
-}
-
-##### GTK3 #####
 
-function make_gtk3 {
-  make_glib
-  make_atk
-  make_pango
-  make_gdk-pixbuf
-  make_cairo
-  make_libepoxy
-  build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/gtk+/3.22  gtk+-3.22.30  tar.xz  true
+      make_glib
+      make_atk
+      make_pango
+      make_gdk-pixbuf
+      make_cairo
+      make_libepoxy
+      build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/gtk+/3.24  gtk+-3.24.5  tar.xz  true
+  fi
 
   # make all incl. tests and examples runs through fine
   # make install fails with issue with
@@ -918,17 +906,17 @@ function make_libxml2 {
   fi
 }
 
-##### GTK-SOURCEVIEW2 #####
+##### GTK-SOURCEVIEW3 #####
 
-function make_gtk_sourceview2 {
+function make_gtk_sourceview3 {
   # Cygwin packet dependencies: intltool
   # gtksourceview-2.11.2 requires GTK2
   # gtksourceview-2.91.9 requires GTK3
   # => We use gtksourceview-2.11.2 which seems to be the newest GTK2 based one
   if [ "$GTK_FROM_SOURCES" == "Y" ]; then
-    make_gtk2
+    make_gtk3
     make_libxml2
-    build_conf_make_inst  https://download.gnome.org/sources/gtksourceview/2.11  gtksourceview-2.11.2  tar.bz2  true
+    build_conf_make_inst  https://download.gnome.org/sources/gtksourceview/3.24  gtksourceview-3.24.9  tar.bz2  true
   fi
 }
 
@@ -1018,7 +1006,7 @@ function make_ln {
 
 function make_ocaml {
   get_flex_dll_link_bin
-  if build_prep https://github.com/ocaml/ocaml/archive 4.07.0 tar.gz 1 ocaml-4.07.0 ; then
+  if build_prep https://github.com/ocaml/ocaml/archive 4.07.1 tar.gz 1 ocaml-4.07.1 ; then
     # See README.win32.adoc
     cp config/m-nt.h byterun/caml/m.h
     cp config/s-nt.h byterun/caml/s.h
@@ -1073,7 +1061,6 @@ function make_ocaml {
 
 function make_ocaml_tools {
   make_findlib
-  # make_camlp5
 }
 
 ##### OCAML EXTRA LIBRARIES #####
@@ -1081,8 +1068,7 @@ function make_ocaml_tools {
 function make_ocaml_libs {
   make_num
   make_findlib
-  make_lablgtk
-  # make_stdint
+  # make_lablgtk
 }
 
 ##### Ocaml num library #####
@@ -1130,6 +1116,20 @@ function make_findlib {
   fi
 }
 
+##### Dune build system #####
+
+function make_dune {
+  make_ocaml
+
+  if build_prep https://github.com/ocaml/dune/archive/ 1.6.3 tar.gz 1 ; then
+
+    log2 make release
+    log2 make install
+
+    build_post
+  fi
+}
+
 ##### MENHIR Ocaml Parser Generator #####
 
 function make_menhir {
@@ -1144,108 +1144,50 @@ function make_menhir {
   fi
 }
 
-##### CAMLP4 Ocaml Preprocessor #####
-
-function make_camlp4 {
-  # OCaml up to 4.01 includes camlp4, from 4.02 it isn't included
-  # Check if command camlp4 exists, if not build camlp4
-  if ! command camlp4 ; then
-    make_ocaml
-    make_findlib
-    if build_prep https://github.com/ocaml/camlp4/archive 4.06+2 tar.gz 1 camlp4-4.06+2 ; then
-      # See https://github.com/ocaml/camlp4/issues/41#issuecomment-112018910
-      logn configure ./configure
-      # Note: camlp4 doesn't support -j 8, so don't pass MAKE_OPT
-      log2 make all
-      log2 make install
-      log2 make clean
-      build_post
-    fi
-  fi
-}
-
-##### CAMLP5 Ocaml Preprocessor #####
-
-function make_camlp5 {
-  make_ocaml
-  make_findlib
-
-  if build_prep https://github.com/camlp5/camlp5/archive rel706 tar.gz 1 camlp5-rel706; then
-    logn configure ./configure
-    # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success
-    sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile
-    # shellcheck disable=SC2086
-    log1 make world.opt $MAKE_OPT
-    log2 make install
-    # For some reason gramlib.a is not copied, but it is required by Coq
-    cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/"
-    # For some reason META is not copied, but it is required by coq_makefile
-    log2 make -C etc META
-    mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/"
-    cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/"
-    log2 make clean
-    build_post
-  fi
-}
-
 ##### LABLGTK Ocaml GTK binding #####
 
 # Note: when rebuilding lablgtk by deleting the .finished file,
 # also delete <root>\usr\x86_64-w64-mingw32\sys-root\mingw\lib\site-lib
 # Otherwise make install fails
 
-function make_lablgtk {
-  make_ocaml
-  make_findlib
-  # make_camlp4 # required by lablgtk-2.18.3 and lablgtk-2.18.5
-  make_gtk2
-  make_gtk_sourceview2
-  if build_prep https://forge.ocamlcore.org/frs/download.php/1726 lablgtk-2.18.6 tar.gz 1 ; then
-    # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe
-    cp "/bin/$TARGET_ARCH-pkg-config"  bin_special/pkg-config
-    logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXOCAML"
-
-    # lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT
+function make_ocaml_cairo2 {
 
-    # lablgtk binary needs to be stripped - otherwise flexdll goes wild
-    # Fix version 1: explicit strip after failed build - this randomly fails in CI
-    # See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html
-    # logn make-world-pre make world || true
-    # $TARGET_ARCH-strip.exe --strip-unneeded src/dlllablgtk2.dll
+  if build_prep https://github.com/Chris00/ocaml-cairo/archive  0.6  tar.gz  1 ; then
 
-    # Fix version 2: Strip by passing linker argument rather than explicit call to strip
-    # See https://github.com/alainfrisch/flexdll/issues/6
-    # Argument to ocamlmklib: -ldopt "-link -Wl,-s"
-    # -ldopt is the okamlmklib linker prefix option
-    # -link is the flexlink linker prefix option
-    # -Wl, is the gcc (linker driver) linker prefix option
-    # -s is the gnu linker option for stripping symbols
-    # These changes are included in dev/build/windows/patches_coq/lablgtk-2.18.3.patch
-
-    log2 make world
+    # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe
+    cp "/bin/$TARGET_ARCH-pkg-config.exe" bin_special/pkg-config.exe
 
-    # lablgtk does not escape FINDLIBDIR path, which can contain backslashes
-    sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make
+    log2 dune build cairo2.install
+    log2 dune install cairo2
 
-    log2 make install
-    log2 make clean
+    log2 dune clean
     build_post
+
   fi
 }
 
-##### Ocaml Stdint #####
-
-function make_stdint {
+function make_lablgtk {
   make_ocaml
   make_findlib
-  if build_prep https://github.com/andrenth/ocaml-stdint/archive 0.3.0 tar.gz 1 Stdint-0.3.0; then
-    # Note: the setup gets the proper install path from ocamlfind, but for whatever reason it wants
-    # to create an empty folder in some folder which defaults to C:\Program Files.
-    # The --preifx overrides this. Id didn't see any files created in /tmp/extra.
-    log_1_3 ocaml setup.ml -configure --prefix /tmp/extra
-    log_1_3 ocaml setup.ml -build
-    log_1_3 ocaml setup.ml -install
-    log_1_3 ocaml setup.ml -clean
+  make_dune
+  make_gtk3
+  make_gtk_sourceview3
+  make_ocaml_cairo2
+
+  if build_prep https://github.com/garrigue/lablgtk/archive  3.0.beta5  tar.gz 1 lablgtk-3.0.beta5 ; then
+
+    # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe
+    cp "/bin/$TARGET_ARCH-pkg-config.exe" bin_special/pkg-config.exe
+
+    # lablgtk3 includes more packages that are not relevant for Coq,
+    # such as gtkspell
+    log2 dune build -p lablgtk3
+    log2 dune install lablgtk3
+
+    log2 dune build -p lablgtk3-sourceview3
+    log2 dune install lablgtk3-sourceview3
+
+    log2 dune clean
     build_post
   fi
 }
@@ -1351,10 +1293,7 @@ function copq_coq_gtk {
     else
       COQSHARE="$PREFIXCOQ/share/"
     fi
-    if [[ ! $COQ_VERSION == 8.4* ]] ; then
-      mv "$COQSHARE"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs"
-      mv "$COQSHARE"*.xml  "$PREFIXCOQ/share/gtksourceview-2.0/styles"
-    fi
+
     mkdir -p "$PREFIXCOQ/ide"
     mv "$COQSHARE"*.png  "$PREFIXCOQ/ide"
     rmdir "$PREFIXCOQ/share/coq" || true
@@ -1383,8 +1322,8 @@ function make_coq {
   make_ocaml
   make_num
   make_findlib
-  # make_camlp5
-  make_lablgtk
+  # Windows build needs tweaks for the GTK3 build
+  # make_lablgtk
   if
     case $COQ_VERSION in
       # e.g. git-v8.6 => download from https://github.com/coq/coq/archive/v8.6.zip
@@ -1436,12 +1375,15 @@ function make_coq {
     fi
 
     log2 make install
-    log1 copy_coq_dlls
+
+    # XXX: Disabled until GTK3 support is back to the build
+    # log1 copy_coq_dlls
+    # log1 copq_coq_gtk
+
     if [ "$INSTALLOCAML" == "Y" ]; then
       copy_coq_objects
     fi
 
-    log1 copq_coq_gtk
     log1 copy_coq_license
 
     # make clean seems to be broken for 8.5pl2
diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch
old mode 100755
new mode 100644
diff --git a/dev/build/windows/patches_coq/flexdll-0.37.patch b/dev/build/windows/patches_coq/flexdll-0.37.patch
new file mode 100644
index 0000000000..82806f9ea4
--- /dev/null
+++ b/dev/build/windows/patches_coq/flexdll-0.37.patch
@@ -0,0 +1,19 @@
+diff/patch file created on Tue, Feb 19, 2019  9:41:26 PM with:
+difftar-folder.sh tarballs/flexdll-0.37.tar.gz flexdll-0.37 1
+TARFILE= tarballs/flexdll-0.37.tar.gz
+FOLDER= flexdll-0.37
+TARSTRIP= 1
+TARPREFIX= flexdll-0.37/
+ORIGFOLDER= flexdll-0.37.orig
+--- flexdll-0.37.orig/cmdline.ml	2017-10-25 10:40:46.000000000 +0200
++++ flexdll-0.37/cmdline.ml	2019-02-19 21:41:18.157024900 +0100
+@@ -248,6 +248,9 @@
+         String.sub s 0 2 :: String.sub s 2 (String.length s - 2) :: tr rest
+     | s :: rest when String.length s >= 5 && String.sub s 0 5 = "/link" ->
+         "-link" :: String.sub s 5 (String.length s - 5) :: tr rest
++    (* Convert gcc linker option prefix -Wl, to flexlink linker prefix -link *)
++    | s :: rest when String.length s >= 6 && String.sub s 0 5 = "-Wl,-" ->
++        "-link" :: String.sub s 4 (String.length s - 4) :: tr rest
+     | "-arg" :: x :: rest ->
+         tr (Array.to_list (Arg.read_arg x)) @ rest
+     | "-arg0" :: x :: rest ->
diff --git a/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch b/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch
deleted file mode 100644
index 73a098d12a..0000000000
--- a/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch
+++ /dev/null
@@ -1,213 +0,0 @@
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourceiter.c gtksourceview-2.11.2.patched/gtksourceview/gtksourceiter.c
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourceiter.c	2010-05-30 12:24:14.000000000 +0200
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourceiter.c	2015-10-27 14:58:54.422888400 +0100
-***************
-*** 80,86 ****
-  	/* If string contains prefix, check that prefix is not followed
-  	 * by a unicode mark symbol, e.g. that trailing 'a' in prefix
-  	 * is not part of two-char a-with-hat symbol in string. */
-! 	return type != G_UNICODE_COMBINING_MARK &&
-  		type != G_UNICODE_ENCLOSING_MARK &&
-  		type != G_UNICODE_NON_SPACING_MARK;
-  }
---- 80,86 ----
-  	/* If string contains prefix, check that prefix is not followed
-  	 * by a unicode mark symbol, e.g. that trailing 'a' in prefix
-  	 * is not part of two-char a-with-hat symbol in string. */
-! 	return type != G_UNICODE_SPACING_MARK &&
-  		type != G_UNICODE_ENCLOSING_MARK &&
-  		type != G_UNICODE_NON_SPACING_MARK;
-  }
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.c
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.c	2010-05-30 12:24:14.000000000 +0200
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.c	2015-10-27 14:55:30.294477600 +0100
-***************
-*** 274,280 ****
-   * containg a list of language files directories.
-   * The array is owned by @lm and must not be modified.
-   */
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL);
---- 274,280 ----
-   * containg a list of language files directories.
-   * The array is owned by @lm and must not be modified.
-   */
-! const gchar* const *
-  gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL);
-***************
-*** 392,398 ****
-   * available languages or %NULL if no language is available. The array
-   * is owned by @lm and must not be modified.
-   */
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL);
---- 392,398 ----
-   * available languages or %NULL if no language is available. The array
-   * is owned by @lm and must not be modified.
-   */
-! const gchar* const *
-  gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL);
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.h
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.h	2009-11-15 00:41:33.000000000 +0100
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.h	2015-10-27 14:55:30.518500000 +0100
-***************
-*** 62,74 ****
-  
-  GtkSourceLanguageManager *gtk_source_language_manager_get_default		(void);
-  
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  			  gtk_source_language_manager_get_search_path		(GtkSourceLanguageManager *lm);
-  
-  void			  gtk_source_language_manager_set_search_path		(GtkSourceLanguageManager *lm,
-  										 gchar                   **dirs);
-  
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  			  gtk_source_language_manager_get_language_ids		(GtkSourceLanguageManager *lm);
-  
-  GtkSourceLanguage	 *gtk_source_language_manager_get_language		(GtkSourceLanguageManager *lm,
---- 62,74 ----
-  
-  GtkSourceLanguageManager *gtk_source_language_manager_get_default		(void);
-  
-! const gchar* const *
-  			  gtk_source_language_manager_get_search_path		(GtkSourceLanguageManager *lm);
-  
-  void			  gtk_source_language_manager_set_search_path		(GtkSourceLanguageManager *lm,
-  										 gchar                   **dirs);
-  
-! const gchar* const *
-  			  gtk_source_language_manager_get_language_ids		(GtkSourceLanguageManager *lm);
-  
-  GtkSourceLanguage	 *gtk_source_language_manager_get_language		(GtkSourceLanguageManager *lm,
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.c
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.c	2010-05-30 12:24:14.000000000 +0200
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.c	2015-10-27 14:55:30.545502700 +0100
-***************
-*** 310,316 ****
-   *
-   * Since: 2.0
-   */
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME (scheme), NULL);
---- 310,316 ----
-   *
-   * Since: 2.0
-   */
-! const gchar* const *
-  gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME (scheme), NULL);
-***************
-*** 318,324 ****
-  	if (scheme->priv->authors == NULL)
-  		return NULL;
-  
-! 	return (G_CONST_RETURN gchar* G_CONST_RETURN *)scheme->priv->authors->pdata;
-  }
-  
-  /**
---- 318,324 ----
-  	if (scheme->priv->authors == NULL)
-  		return NULL;
-  
-! 	return (const gchar* const *)scheme->priv->authors->pdata;
-  }
-  
-  /**
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.h
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.h	2010-03-29 15:02:56.000000000 +0200
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.h	2015-10-27 14:55:30.565504700 +0100
-***************
-*** 61,67 ****
-  const gchar             *gtk_source_style_scheme_get_name       (GtkSourceStyleScheme *scheme);
-  const gchar             *gtk_source_style_scheme_get_description(GtkSourceStyleScheme *scheme);
-  
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  			 gtk_source_style_scheme_get_authors	(GtkSourceStyleScheme *scheme);
-  
-  const gchar             *gtk_source_style_scheme_get_filename	(GtkSourceStyleScheme *scheme);
---- 61,67 ----
-  const gchar             *gtk_source_style_scheme_get_name       (GtkSourceStyleScheme *scheme);
-  const gchar             *gtk_source_style_scheme_get_description(GtkSourceStyleScheme *scheme);
-  
-! const gchar* const *
-  			 gtk_source_style_scheme_get_authors	(GtkSourceStyleScheme *scheme);
-  
-  const gchar             *gtk_source_style_scheme_get_filename	(GtkSourceStyleScheme *scheme);
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.c
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.c	2010-05-30 12:24:14.000000000 +0200
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.c	2015-10-27 14:55:30.583506500 +0100
-***************
-*** 515,521 ****
-   * of string containing the search path.
-   * The array is owned by the @manager and must not be modified.
-   */
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL);
---- 515,521 ----
-   * of string containing the search path.
-   * The array is owned by the @manager and must not be modified.
-   */
-! const gchar* const *
-  gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL);
-***************
-*** 554,560 ****
-   * of string containing the ids of the available style schemes or %NULL if no
-   * style scheme is available. The array is owned by the @manager and must not be modified.
-   */
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL);
---- 554,560 ----
-   * of string containing the ids of the available style schemes or %NULL if no
-   * style scheme is available. The array is owned by the @manager and must not be modified.
-   */
-! const gchar* const *
-  gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager)
-  {
-  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL);
-diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.h
-*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.h	2009-11-15 00:41:33.000000000 +0100
---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.h	2015-10-27 14:56:24.498897500 +0100
-***************
-*** 73,84 ****
-  void 			 gtk_source_style_scheme_manager_prepend_search_path   (GtkSourceStyleSchemeManager	*manager,
-  						    				 const gchar			*path);
-  
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  			 gtk_source_style_scheme_manager_get_search_path	(GtkSourceStyleSchemeManager	*manager);
-  
-  void			 gtk_source_style_scheme_manager_force_rescan		(GtkSourceStyleSchemeManager	*manager);
-  
-! G_CONST_RETURN gchar* G_CONST_RETURN *
-  			 gtk_source_style_scheme_manager_get_scheme_ids		(GtkSourceStyleSchemeManager	*manager);
-  
-  GtkSourceStyleScheme	*gtk_source_style_scheme_manager_get_scheme		(GtkSourceStyleSchemeManager	*manager,
---- 73,84 ----
-  void 			 gtk_source_style_scheme_manager_prepend_search_path   (GtkSourceStyleSchemeManager	*manager,
-  						    				 const gchar			*path);
-  
-! const gchar* const *
-  			 gtk_source_style_scheme_manager_get_search_path	(GtkSourceStyleSchemeManager	*manager);
-  
-  void			 gtk_source_style_scheme_manager_force_rescan		(GtkSourceStyleSchemeManager	*manager);
-  
-! const gchar* const *
-  			 gtk_source_style_scheme_manager_get_scheme_ids		(GtkSourceStyleSchemeManager	*manager);
-  
-  GtkSourceStyleScheme	*gtk_source_style_scheme_manager_get_scheme		(GtkSourceStyleSchemeManager	*manager,
diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.6.patch b/dev/build/windows/patches_coq/lablgtk-2.18.6.patch
deleted file mode 100644
index 23c303135d..0000000000
--- a/dev/build/windows/patches_coq/lablgtk-2.18.6.patch
+++ /dev/null
@@ -1,101 +0,0 @@
-diff/patch file created on Wed, Apr 25, 2018 11:08:05 AM with:
-difftar-folder.sh ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz lablgtk-2.18.3 1
-TARFILE= ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz
-FOLDER= lablgtk-2.18.3
-TARSTRIP= 1
-TARPREFIX= lablgtk-2.18.3/
-ORIGFOLDER= lablgtk-2.18.3.orig
---- lablgtk-2.18.3.orig/configure	2014-10-29 08:51:05.000000000 +0100
-+++ lablgtk-2.18.3/configure	2018-04-25 10:58:54.454501600 +0200
-@@ -2667,7 +2667,7 @@
- fi
- 
- 
--if test "`$OCAMLFIND printconf stdlib`" != "`$CAMLC -where`"; then
-+if test "`$OCAMLFIND printconf stdlib | tr '\\' '/'`" != "`$CAMLC -where | tr '\\' '/'`"; then
-   { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5
- $as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;}
-   OCAMLFIND=no
---- lablgtk-2.18.3.orig/src/glib.mli	2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3/src/glib.mli	2018-04-25 10:58:54.493555500 +0200
-@@ -75,6 +75,7 @@
-   type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI]
-   type id
-   val channel_of_descr : Unix.file_descr -> channel
-+  val channel_of_descr_socket : Unix.file_descr -> channel
-   val add_watch :
-     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
-   val remove : id -> unit
---- lablgtk-2.18.3.orig/src/glib.ml	2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3/src/glib.ml	2018-04-25 10:58:54.479543500 +0200
-@@ -72,6 +72,8 @@
-   type id
-   external channel_of_descr : Unix.file_descr -> channel
-     = "ml_g_io_channel_unix_new"
-+  external channel_of_descr_socket : Unix.file_descr -> channel
-+    = "ml_g_io_channel_unix_new_socket"
-   external remove : id -> unit = "ml_g_source_remove"
-   external add_watch :
-     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
---- lablgtk-2.18.3.orig/src/Makefile	2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3/src/Makefile	2018-04-25 10:58:54.506522500 +0200
-@@ -461,9 +461,9 @@
- 	  do rm -f "$(BINDIR)"/$$f; done
- 
- lablgtk.cma liblablgtk2$(XA): $(COBJS) $(MLOBJS)
--	$(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
-+	$(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
- lablgtk.cmxa: $(COBJS) $(MLOBJS:.cmo=.cmx)
--	$(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
-+	$(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS)
- lablgtk.cmxs: DYNLINKLIBS=$(GTK_LIBS)
- 
- lablgtkgl.cma liblablgtkgl2$(XA): $(GLCOBJS) $(GLMLOBJS)
---- lablgtk-2.18.3.orig/src/ml_glib.c	2014-10-29 08:51:06.000000000 +0100
-+++ lablgtk-2.18.3/src/ml_glib.c	2018-04-25 10:58:54.539535600 +0200
-@@ -25,6 +25,8 @@
- #include <string.h>
- #include <locale.h>
- #ifdef _WIN32
-+/* to kill a #warning: include winsock2.h before windows.h */
-+#include <winsock2.h>
- #include "win32.h"
- #include <wtypes.h>
- #include <io.h>
-@@ -38,6 +40,11 @@
- #include <caml/callback.h>
- #include <caml/threads.h>
- 
-+#ifdef _WIN32
-+/* for Socket_val */
-+#include <caml/unixsupport.h>
-+#endif
-+
- #include "wrappers.h"
- #include "ml_glib.h"
- #include "glib_tags.h"
-@@ -325,14 +332,23 @@
- 
- #ifndef _WIN32
- ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref)
-+CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) {
-+  return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1))); 
-+}
- 
- #else
- CAMLprim value ml_g_io_channel_unix_new(value wh)
- {
-   return Val_GIOChannel_noref
--    (g_io_channel_unix_new
-+    (g_io_channel_win32_new_fd
-      (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY)));
- }
-+
-+CAMLprim value ml_g_io_channel_unix_new_socket(value wh)
-+{
-+  return Val_GIOChannel_noref
-+    (g_io_channel_win32_new_socket(Socket_val(wh)));
-+}
- #endif
- 
- static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c,
diff --git a/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch b/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch
new file mode 100644
index 0000000000..1c6a038da9
--- /dev/null
+++ b/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch
@@ -0,0 +1,76 @@
+diff/patch file created on Wed, Feb 20, 2019 11:29:48 AM with:
+difftar-folder.sh tarballs/lablgtk-3.0.beta4.tar.gz lablgtk-3.0.beta4 1
+TARFILE= tarballs/lablgtk-3.0.beta4.tar.gz
+FOLDER= lablgtk-3.0.beta4
+TARSTRIP= 1
+TARPREFIX= lablgtk-3.0.beta4/
+ORIGFOLDER= lablgtk-3.0.beta4.orig
+--- lablgtk-3.0.beta4.orig/src/glib.ml	2019-02-11 07:08:17.000000000 +0100
++++ lablgtk-3.0.beta4/src/glib.ml	2019-02-20 11:28:28.439137100 +0100
+@@ -72,6 +72,8 @@
+   type id
+   external channel_of_descr : Unix.file_descr -> channel
+     = "ml_g_io_channel_unix_new"
++  external channel_of_descr_socket : Unix.file_descr -> channel
++    = "ml_g_io_channel_unix_new_socket"
+   external remove : id -> unit = "ml_g_source_remove"
+   external add_watch :
+     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
+--- lablgtk-3.0.beta4.orig/src/glib.mli	2019-02-11 07:08:17.000000000 +0100
++++ lablgtk-3.0.beta4/src/glib.mli	2019-02-20 11:28:28.423592200 +0100
+@@ -75,6 +75,7 @@
+   type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI]
+   type id
+   val channel_of_descr : Unix.file_descr -> channel
++  val channel_of_descr_socket : Unix.file_descr -> channel
+   val add_watch :
+     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
+   val remove : id -> unit
+--- lablgtk-3.0.beta4.orig/src/ml_glib.c	2019-02-11 07:08:17.000000000 +0100
++++ lablgtk-3.0.beta4/src/ml_glib.c	2019-02-20 11:28:28.455395900 +0100
+@@ -25,6 +25,8 @@
+ #include <string.h>
+ #include <locale.h>
+ #ifdef _WIN32
++/* to kill a #warning: include winsock2.h before windows.h */
++#include <winsock2.h>
+ #include "win32.h"
+ #include <wtypes.h>
+ #include <io.h>
+@@ -38,6 +40,11 @@
+ #include <caml/callback.h>
+ #include <caml/threads.h>
+ 
++#ifdef _WIN32
++/* for Socket_val */
++#include <caml/unixsupport.h>
++#endif
++
+ #include "wrappers.h"
+ #include "ml_glib.h"
+ #include "glib_tags.h"
+@@ -326,14 +333,23 @@
+ 
+ #ifndef _WIN32
+ ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref)
++CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) {
++  return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1))); 
++}
+ 
+ #else
+ CAMLprim value ml_g_io_channel_unix_new(value wh)
+ {
+   return Val_GIOChannel_noref
+-    (g_io_channel_unix_new
++    (g_io_channel_win32_new_fd
+      (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY)));
+ }
++
++CAMLprim value ml_g_io_channel_unix_new_socket(value wh)
++{
++  return Val_GIOChannel_noref
++    (g_io_channel_win32_new_socket(Socket_val(wh)));
++}
+ #endif
+ 
+ static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c,
diff --git a/dev/build/windows/patches_coq/quickchick.patch b/dev/build/windows/patches_coq/quickchick.patch
old mode 100755
new mode 100644
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index c95bcf5573..e553cbed1b 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-03-11-V1"
+# CACHEKEY: "bionic_coq-V2019-03-12-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -10,7 +10,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         # Dependencies of the image, the test-suite and external projects
         m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \
         # Dependencies of lablgtk (for CoqIDE)
-        libgtk3.0-dev libgtksourceview3.0-dev \
+        libgtksourceview-3.0-dev \
         # Dependencies of stdlib and sphinx doc
         texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
         xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \
@@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \
                  antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
 
 # We need to install OPAM 2.0 manually for now.
-RUN wget https://github.com/ocaml/opam/releases/download/2.0.0/opam-2.0.0-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+RUN wget https://github.com/ocaml/opam/releases/download/2.0.3/opam-2.0.3-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
 
 # Basic OPAM setup
 ENV NJOBS="2" \
@@ -41,7 +41,10 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \
     CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
-ENV COQIDE_OPAM="lablgtk3 conf-gtksourceview3"
+ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
+
+# Must add this to COQIDE_OPAM{,_EDGE} when we update the opam
+# packages "lablgtk3-gtksourceview3"
 
 # base switch
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
@@ -53,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.07.1" \
-    COQIDE_OPAM_EDGE="lablgtk3 conf-gtksourceview3" \
+    COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" \
     BASE_OPAM_EDGE="dune-release.1.1.0"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
diff --git a/ide/dune b/ide/dune
index 5082d84c4f..e3e61609af 100644
--- a/ide/dune
+++ b/ide/dune
@@ -29,7 +29,7 @@
  (wrapped false)
  (modules (:standard \ document fake_ide idetop coqide_main))
  (optional)
- (libraries coqide-server.protocol coqide-server.core lablgtk3.sourceview3))
+ (libraries coqide-server.protocol coqide-server.core lablgtk3-sourceview3))
 
 (rule
  (targets coqide_os_specific.ml)
diff --git a/ide/ide.mllib b/ide/ide.mllib
index a7ade71307..30ac5c9ad7 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,7 +9,6 @@ Config_lexer
 Utf8_convert
 Preferences
 Project_file
-Topfmt
 Ideutils
 Coq
 Coq_lex
diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml
index d753687077..755a42eadd 100644
--- a/ide/wg_Detachable.ml
+++ b/ide/wg_Detachable.ml
@@ -15,6 +15,9 @@ class type detachable_signals =
     method detached : callback:(GObj.widget -> unit) -> unit
   end
 
+(* Cannot do a local warning in 4.05.0, fixme when we use a newer
+   OCaml to avoid the warning in the method itself. *)
+[@@@ocaml.warning "-7"]
 class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) =
 
   object(self)
-- 
cgit v1.2.3


From 1f4a9071b3236b61642cbd5cf35f82a8fb15bf32 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Mon, 25 Feb 2019 11:54:28 +0100
Subject: [win] Mostly fixed GTK3 CoqIDE Windows build (icons don't work, only
 64 but tested, only binary GTK)

---
 dev/build/windows/makecoq_mingw.sh | 75 +++++++++++++++++++-------------------
 1 file changed, 37 insertions(+), 38 deletions(-)

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 03bda8d0c0..da6a8997a9 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -965,7 +965,7 @@ function get_flex_dll_link_bin {
 # Build flexdll and flexlink from sources after building OCaml
 
 function make_flex_dll_link {
-  if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip ; then
+  if build_prep https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 ; then
     if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
       # shellcheck disable=SC2086
       log1 make $MAKE_OPT build_mingw flexlink.exe
@@ -1068,7 +1068,7 @@ function make_ocaml_tools {
 function make_ocaml_libs {
   make_num
   make_findlib
-  # make_lablgtk
+  make_lablgtk
 }
 
 ##### Ocaml num library #####
@@ -1121,7 +1121,7 @@ function make_findlib {
 function make_dune {
   make_ocaml
 
-  if build_prep https://github.com/ocaml/dune/archive/ 1.6.3 tar.gz 1 ; then
+  if build_prep https://github.com/ocaml/dune/archive/ 1.6.3 tar.gz 1 dune-1.6.3 ; then
 
     log2 make release
     log2 make install
@@ -1152,10 +1152,10 @@ function make_menhir {
 
 function make_ocaml_cairo2 {
 
-  if build_prep https://github.com/Chris00/ocaml-cairo/archive  0.6  tar.gz  1 ; then
+  if build_prep https://github.com/Chris00/ocaml-cairo/archive 0.6 tar.gz 1 ocaml_cairo2-0.6; then
 
-    # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe
-    cp "/bin/$TARGET_ARCH-pkg-config.exe" bin_special/pkg-config.exe
+    # configure should be fixed to search for $TARGET_ARCH-pkg-config
+    cp "/bin/$TARGET_ARCH-pkg-config" bin_special/pkg-config
 
     log2 dune build cairo2.install
     log2 dune install cairo2
@@ -1176,8 +1176,8 @@ function make_lablgtk {
 
   if build_prep https://github.com/garrigue/lablgtk/archive  3.0.beta5  tar.gz 1 lablgtk-3.0.beta5 ; then
 
-    # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe
-    cp "/bin/$TARGET_ARCH-pkg-config.exe" bin_special/pkg-config.exe
+    # configure should be fixed to search for $TARGET_ARCH-pkg-config
+    cp "/bin/$TARGET_ARCH-pkg-config" bin_special/pkg-config
 
     # lablgtk3 includes more packages that are not relevant for Coq,
     # such as gtkspell
@@ -1212,42 +1212,44 @@ function copy_coq_dlls {
   # Select all missing DLLs from the module list, right click "copy filenames"
   # Delay loaded DLLs from Windows can be ignored (hour-glass icon at begin of line)
   # Do this recursively until there are no further missing DLLs (File close + reopen)
-  # For running this quickly, just do "cd coq-<ver> ; call copy_coq_dlls ; cd .." at the end of this script.
+  # For running this quickly, just do "cd coq-<ver> ; copy_coq_dlls ; cd .." at the end of this script.
   # Do the same for coqc and ocamlc (usually doesn't result in additional files)
 
-  copy_coq_dll LIBATK-1.0-0.DLL
   copy_coq_dll LIBCAIRO-2.DLL
-  copy_coq_dll LIBEXPAT-1.DLL
-  copy_coq_dll LIBFFI-6.DLL
   copy_coq_dll LIBFONTCONFIG-1.DLL
   copy_coq_dll LIBFREETYPE-6.DLL
-  copy_coq_dll LIBGDK-WIN32-2.0-0.DLL
+  copy_coq_dll LIBGDK-3-0.DLL
   copy_coq_dll LIBGDK_PIXBUF-2.0-0.DLL
-  copy_coq_dll LIBGIO-2.0-0.DLL
   copy_coq_dll LIBGLIB-2.0-0.DLL
-  copy_coq_dll LIBGMODULE-2.0-0.DLL
   copy_coq_dll LIBGOBJECT-2.0-0.DLL
-  copy_coq_dll LIBGTK-WIN32-2.0-0.DLL
-  copy_coq_dll LIBINTL-8.DLL
+  copy_coq_dll LIBGTK-3-0.DLL
+  copy_coq_dll LIBGTKSOURCEVIEW-3.0-1.DLL
   copy_coq_dll LIBPANGO-1.0-0.DLL
+  copy_coq_dll LIBATK-1.0-0.DLL
+  copy_coq_dll LIBBZ2-1.DLL
+  copy_coq_dll LIBCAIRO-GOBJECT-2.DLL
+  copy_coq_dll LIBEPOXY-0.DLL
+  copy_coq_dll LIBEXPAT-1.DLL
+  copy_coq_dll LIBFFI-6.DLL
+  copy_coq_dll LIBGIO-2.0-0.DLL
+  copy_coq_dll LIBGMODULE-2.0-0.DLL
+  copy_coq_dll LIBINTL-8.DLL
   copy_coq_dll LIBPANGOCAIRO-1.0-0.DLL
   copy_coq_dll LIBPANGOWIN32-1.0-0.DLL
-  copy_coq_dll libpcre-1.dll
+  copy_coq_dll LIBPCRE-1.DLL
   copy_coq_dll LIBPIXMAN-1-0.DLL
   copy_coq_dll LIBPNG16-16.DLL
   copy_coq_dll LIBXML2-2.DLL
   copy_coq_dll ZLIB1.DLL
+  copy_coq_dll ICONV.DLL
+  copy_coq_dll LIBLZMA-5.DLL
+  copy_coq_dll LIBPANGOFT2-1.0-0.DLL
+  copy_coq_dll LIBHARFBUZZ-0.DLL
 
   # Depends on if GTK is built from sources
   if [ "$GTK_FROM_SOURCES" == "Y" ]; then
-    copy_coq_dll libiconv-2.dll
-  else
-    copy_coq_dll ICONV.DLL
-    copy_coq_dll LIBBZ2-1.DLL
-    copy_coq_dll LIBGTKSOURCEVIEW-2.0-0.DLL
-    copy_coq_dll LIBHARFBUZZ-0.DLL
-    copy_coq_dll LIBLZMA-5.DLL
-    copy_coq_dll LIBPANGOFT2-1.0-0.DLL
+    echo "Building GTK from sources is currently not supported"
+    exit 1
   fi;
 
   # Architecture dependent files
@@ -1277,14 +1279,14 @@ function copy_coq_objects {
 
 # Copy required GTK config and suport files
 
-function copq_coq_gtk {
-  echo 'gtk-theme-name = "MS-Windows"'     >  "$PREFIX/etc/gtk-2.0/gtkrc"
-  echo 'gtk-fallback-icon-theme = "Tango"' >> "$PREFIX/etc/gtk-2.0/gtkrc"
+function copy_coq_gtk {
+  echo 'gtk-theme-name = "Default"'     >  "$PREFIX/etc/gtk-3.0/gtkrc"
+  echo 'gtk-fallback-icon-theme = "Tango"' >> "$PREFIX/etc/gtk-3.0/gtkrc"
 
   if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
-    install_glob "$PREFIX/etc/gtk-2.0" '*'                            "$PREFIXCOQ/gtk-2.0"
-    install_glob "$PREFIX/share/gtksourceview-2.0/language-specs" '*' "$PREFIXCOQ/share/gtksourceview-2.0/language-specs"
-    install_glob "$PREFIX/share/gtksourceview-2.0/styles" '*'         "$PREFIXCOQ/share/gtksourceview-2.0/styles"
+    install_glob "$PREFIX/etc/gtk-3.0" '*'                            "$PREFIXCOQ/gtk-3.0"
+    install_glob "$PREFIX/share/gtksourceview-3.0/language-specs" '*' "$PREFIXCOQ/share/gtksourceview-3.0/language-specs"
+    install_glob "$PREFIX/share/gtksourceview-3.0/styles" '*'         "$PREFIXCOQ/share/gtksourceview-3.0/styles"
     install_rec  "$PREFIX/share/themes" '*'                           "$PREFIXCOQ/share/themes"
 
     # This below item look like a bug in make install
@@ -1322,8 +1324,7 @@ function make_coq {
   make_ocaml
   make_num
   make_findlib
-  # Windows build needs tweaks for the GTK3 build
-  # make_lablgtk
+  make_lablgtk
   if
     case $COQ_VERSION in
       # e.g. git-v8.6 => download from https://github.com/coq/coq/archive/v8.6.zip
@@ -1375,10 +1376,8 @@ function make_coq {
     fi
 
     log2 make install
-
-    # XXX: Disabled until GTK3 support is back to the build
-    # log1 copy_coq_dlls
-    # log1 copq_coq_gtk
+    log1 copy_coq_dlls
+    log1 copy_coq_gtk
 
     if [ "$INSTALLOCAML" == "Y" ]; then
       copy_coq_objects
-- 
cgit v1.2.3


From cef009d27d79b90ee42e0ea96c487d5a07d803de Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Mon, 18 Mar 2019 11:04:00 +0100
Subject: Fixed incompatibility between new cygwin pkg-config and dune

---
 dev/build/windows/makecoq_mingw.sh         | 20 ++++++++++++--------
 dev/build/windows/patches_coq/pkg-config.c | 29 +++++++++++++++++++++++++++++
 2 files changed, 41 insertions(+), 8 deletions(-)
 create mode 100755 dev/build/windows/patches_coq/pkg-config.c

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index da6a8997a9..4c5bd29236 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1002,6 +1002,16 @@ function make_ln {
   fi
 }
 
+##### ARCH-pkg-config replacement #####
+
+# cygwin replaced ARCH-pkg-config with a shell script, which doesn't work e.g. for dune on Windows.
+# This builds a binary replacement for the shell script and puts it into the bin_special folder.
+# There is no global installation since it is module specific what pkg-config is needed under what name.
+
+function make_arch_pkg_config {
+  gcc -DARCH="$TARGET_ARCH" -o bin_special/pkg-config.exe $PATCHES/pkg-config.c
+}
+
 ##### OCAML #####
 
 function make_ocaml {
@@ -1151,15 +1161,11 @@ function make_menhir {
 # Otherwise make install fails
 
 function make_ocaml_cairo2 {
-
   if build_prep https://github.com/Chris00/ocaml-cairo/archive 0.6 tar.gz 1 ocaml_cairo2-0.6; then
-
-    # configure should be fixed to search for $TARGET_ARCH-pkg-config
-    cp "/bin/$TARGET_ARCH-pkg-config" bin_special/pkg-config
+    make_arch_pkg_config
 
     log2 dune build cairo2.install
     log2 dune install cairo2
-
     log2 dune clean
     build_post
 
@@ -1175,9 +1181,7 @@ function make_lablgtk {
   make_ocaml_cairo2
 
   if build_prep https://github.com/garrigue/lablgtk/archive  3.0.beta5  tar.gz 1 lablgtk-3.0.beta5 ; then
-
-    # configure should be fixed to search for $TARGET_ARCH-pkg-config
-    cp "/bin/$TARGET_ARCH-pkg-config" bin_special/pkg-config
+    make_arch_pkg_config
 
     # lablgtk3 includes more packages that are not relevant for Coq,
     # such as gtkspell
diff --git a/dev/build/windows/patches_coq/pkg-config.c b/dev/build/windows/patches_coq/pkg-config.c
new file mode 100755
index 0000000000..e4fdcd4d7d
--- /dev/null
+++ b/dev/build/windows/patches_coq/pkg-config.c
@@ -0,0 +1,29 @@
+// MinGW personality wrapper for pkgconf
+// This is an excutable replacement for the shell scripts /bin/ARCH-pkg-config
+// Compile with e.g.
+// gcc pkg-config.c -DARCH=x86_64-w64-mingw32 -o pkg-config.exe
+// gcc pkg-config.c -DARCH=i686-w64-mingw32 -o pkg-config.exe
+// ATTENTION: Do not compile with MinGW-gcc, compile with cygwin gcc!
+//
+// To test it execute e.g.
+// $ ./pkg-config --path zlib
+// /usr/x86_64-w64-mingw32/sys-root/mingw/lib/pkgconfig/zlib.pc
+
+#include <unistd.h>
+
+#define STRINGIFY1(arg) #arg
+#define STRINGIFY(arg) STRINGIFY1(arg)
+
+int main(int argc, char *argv[])
+{
+    // +1 for extra argument, +1 for trailing NULL
+    char * argvnew[argc+2];
+    int id=0, is=0;
+
+    argvnew[id++] = argv[is++];
+    argvnew[id++] = "--personality="STRINGIFY(ARCH);
+    while( is<argc ) argvnew[id++] = argv[is++];
+    argvnew[id++] = 0;
+
+    return execv("/usr/bin/pkgconf", argvnew);
+}
-- 
cgit v1.2.3