diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2015-12-14 13:33:47 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2015-12-14 13:37:01 +0100 |
commit | 469cb750c6c1aa46f77b2a89a36f79f29aa97073 (patch) | |
tree | 03ea46d4888936d910b2c56e82b64859b10e5832 | |
parent | c377938a8f87d9c0517aa0c7d4564323951a2133 (diff) |
Revert PMP's fix of #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:
490160d25d3caac1d2ea5beebbbebc959b1b3832.
ef8718a7fd3bcd960d954093d8c636525e6cc492.
6f9cc3aca5bb0e5684268a7283796a9272ed5f9d.
901a9b29adf507370732aeafbfea6718c1842f1b.
-rw-r--r-- | INSTALL.ide | 2 | ||||
-rw-r--r-- | configure.ml | 50 | ||||
-rw-r--r-- | ide/preferences.ml | 31 |
3 files changed, 14 insertions, 69 deletions
diff --git a/INSTALL.ide b/INSTALL.ide index b651e77db..6e41b2d05 100644 --- a/INSTALL.ide +++ b/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 diff --git a/configure.ml b/configure.ml index 3a55fb570..51033c3d0 100644 --- a/configure.ml +++ b/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,11 +736,11 @@ 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 @@ -756,34 +748,10 @@ let get_lablgtkdir () = 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"); diff --git a/ide/preferences.ml b/ide/preferences.ml index 90862d064..01ce45483 100644 --- a/ide/preferences.ml +++ b/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) |