Revert PMP's fix of rocq-prover#2498, which introduces an incompatibility with lablgtk

2.14. Debian ships with lablgtk 2.16 only since a few months, so we apply the
fix to trunk instead.

This reverts commits:
490160d.
ef8718a.
6f9cc3a.
901a9b2.

Author: maximedenes

INSTALL.ide

@@ -39,7 +39,7 @@ COMPILATION REQUIREMENTS
   install GTK+ 2.x, should you need to force it for one reason
   or another.)
 - The OCaml bindings for GTK+ 2.x, lablgtk2 with support for gtksourceview2.
-  You need at least version 2.16.
+  You need at least version 2.14.2.
 
   Your distribution may contain precompiled packages. For example, for
   Debian, run

configure.ml

@@ -719,18 +719,10 @@ let operating_system, osdeplibs =
 
 (** * lablgtk2 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 check_lablgtkdir ?(fatal=false) msg dir =
   let yell msg = if fatal then die msg else (printf "%s\n" 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")) then
@@ -744,46 +736,22 @@ let check_lablgtkdir ?(fatal=false) src dir =
 let get_lablgtkdir () =
   match !Prefs.lablgtkdir with
   | Some dir ->
-    let msg = Manual in
+    let msg = "manually provided" in
     if check_lablgtkdir ~fatal:true msg dir then dir, msg
-    else "", msg
+    else "", ""
   | None ->
-    let msg = OCamlFind in
+    let msg = "via ocamlfind" in
     let d1,_ = tryrun "ocamlfind" ["query";"lablgtk2.sourceview2"] in
     if d1 <> "" && check_lablgtkdir msg d1 then d1, msg
     else
       (* In debian wheezy, ocamlfind knows only of lablgtk2 *)
       let d2,_ = tryrun "ocamlfind" ["query";"lablgtk2"] in
       if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg
       else
-        let msg = Stdlib in
+        let msg = "in OCaml library" in
         let d3 = camllib^"/lablgtk2" in
         if check_lablgtkdir msg d3 then d3, msg
-        else "", msg
-
-(** Detect and/or verify the Lablgtk2 version *)
-
-let check_lablgtk_version src dir = match src with
-| Manual | Stdlib ->
-  let test accu f =
-    if accu then
-      let test = sprintf "grep -q -w %s %S/glib.mli" f dir in
-      Sys.command test = 0
-    else false
-  in
-  let heuristics = [
-    "convert_with_fallback";
-    "wrap_poll_func"; (** Introduced in lablgtk 2.16 *)
-  ] in
-  let ans = List.fold_left test true heuristics in
-  if ans then printf "Warning: could not check the version of lablgtk2.\n";
-  (ans, "an unknown version")
-| OCamlFind ->
-  let v, _ = tryrun "ocamlfind" ["query"; "-format"; "%v"; "lablgtk2"] in
-  try
-    let vi = List.map s2i (numeric_prefix_list v) in
-    ([2; 16] <= vi, v)
-  with _ -> (false, v)
+        else "", ""
 
 let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native"
 
@@ -807,9 +775,9 @@ 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";
-  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.16, found " ^ version ^ ")");
+  let found = sprintf "LablGtk2 found (%s)" via in
+  let test = sprintf "grep -q -w convert_with_fallback %S/glib.mli" dir in
+  if Sys.command test <> 0 then set_ide No (found^" but too old");
   (* 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");

ide/preferences.ml

@@ -711,61 +711,38 @@ let configure ?(apply=(fun () -> ())) () =
       ~f:(fun s -> current.project_file_name <- s)
       current.project_file_name
   in
-  let update_modifiers prefix mds =
-    let change ~path ~key ~modi ~changed =
-      if CString.is_sub prefix path 0 then
-        ignore (GtkData.AccelMap.change_entry ~key ~modi:mds ~replace:true path)
-    in
-    GtkData.AccelMap.foreach change
-  in
   let help_string =
     "restart to apply"
   in
   let the_valid_mod = str_to_mod_list current.modifiers_valid in
   let modifier_for_tactics =
-    let cb l =
-      current.modifier_for_tactics <- mod_list_to_str l;
-      update_modifiers "<Actions>/Tactics/" l
-    in
     modifiers
       ~allow:the_valid_mod
-      ~f:cb
+      ~f:(fun l -> current.modifier_for_tactics <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for Tactics Menu"
       (str_to_mod_list current.modifier_for_tactics)
   in
   let modifier_for_templates =
-    let cb l =
-      current.modifier_for_templates <- mod_list_to_str l;
-      update_modifiers "<Actions>/Templates/" l
-    in
     modifiers
       ~allow:the_valid_mod
-      ~f:cb
+      ~f:(fun l -> current.modifier_for_templates <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for Templates Menu"
       (str_to_mod_list current.modifier_for_templates)
   in
   let modifier_for_navigation =
-    let cb l =
-      current.modifier_for_navigation <- mod_list_to_str l;
-      update_modifiers "<Actions>/Navigation/" l
-    in
     modifiers
       ~allow:the_valid_mod
-      ~f:cb
+      ~f:(fun l -> current.modifier_for_navigation <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for Navigation Menu"
       (str_to_mod_list current.modifier_for_navigation)
   in
   let modifier_for_display =
-    let cb l =
-      current.modifier_for_display <- mod_list_to_str l;
-      update_modifiers "<Actions>/View/" l
-    in
     modifiers
       ~allow:the_valid_mod
-      ~f:cb
+      ~f:(fun l -> current.modifier_for_display <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for View Menu"
       (str_to_mod_list current.modifier_for_display)