diff options
| author | Pierre-Marie Pédrot | 2019-03-19 15:46:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-19 15:46:13 +0100 |
| commit | 2b68b2223527b5bc247bd338ae4613a00654636c (patch) | |
| tree | 940db9f99a47fa996c1374446f6d944ca5183d21 | |
| parent | f1ca51445650a6595a9dfd28c365b83fa25d1eea (diff) | |
| parent | cef009d27d79b90ee42e0ea96c487d5a07d803de (diff) | |
Merge PR #9279: CoqIDE on lablgtk3
Ack-by: MSoegtropIMC
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: garrigue
Ack-by: herbelin
45 files changed, 420 insertions, 709 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b6e7f8aeef..fd94051a37 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/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. @@ -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..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 +lablgtk2 #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,lablgtk2.sourceview2 $(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,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 +131,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 +231,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 8b6fccb5e3..5b99851f83 100644 --- a/configure.ml +++ b/configure.ml @@ -150,7 +150,11 @@ 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"] + | [v1;v2;""] -> [v1;v2;"0"] (* e.g. because it ends with ".beta" *) + | v -> v (** Combined existence and directory tests *) @@ -226,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; @@ -263,7 +266,6 @@ let default = { docdir = None; coqdocdir = None; ocamlfindcmd = None; - lablgtkdir = None; arch = None; natdynlink = true; coqide = None; @@ -368,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 }), @@ -697,75 +697,31 @@ let check_for_numlib () = let numlib = check_for_numlib () -(** * lablgtk2 and CoqIDE *) +(** * 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")) 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";"lablgtk2.sourceview2"] 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 - if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg - else - let msg = Stdlib in - let d3 = camllib^"/lablgtk2" 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 lablgtk2.\nMake sure your version is at least 2.18.3."; - (true, "an unknown version") -| OCamlFind -> - let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in - try - let vi = List.map s2i (numeric_prefix_list v) in - if vi < [2; 16; 0] then +let check_lablgtk_version () = + let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk3"] 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 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) +*) let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native" @@ -788,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 "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.18.3, 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 () @@ -808,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 @@ -1011,7 +964,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; @@ -1203,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 314943a881..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-gtksourceview" - "lablgtk" { >= "2.18.5" } + "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..4c5bd29236 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 } @@ -977,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 @@ -1014,11 +1002,21 @@ 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 { 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 +1071,6 @@ function make_ocaml { function make_ocaml_tools { make_findlib - # make_camlp5 } ##### OCAML EXTRA LIBRARIES ##### @@ -1082,7 +1079,6 @@ function make_ocaml_libs { make_num make_findlib make_lablgtk - # make_stdint } ##### Ocaml num library ##### @@ -1130,6 +1126,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 dune-1.6.3 ; then + + log2 make release + log2 make install + + build_post + fi +} + ##### MENHIR Ocaml Parser Generator ##### function make_menhir { @@ -1144,108 +1154,44 @@ 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 - - # 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 - - # 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 - - # lablgtk does not escape FINDLIBDIR path, which can contain backslashes - sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make +function make_ocaml_cairo2 { + if build_prep https://github.com/Chris00/ocaml-cairo/archive 0.6 tar.gz 1 ocaml_cairo2-0.6; then + make_arch_pkg_config - log2 make install - log2 make clean + log2 dune build cairo2.install + log2 dune install cairo2 + 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 + make_arch_pkg_config + + # 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 } @@ -1270,42 +1216,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 @@ -1335,14 +1283,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 @@ -1351,10 +1299,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,7 +1328,6 @@ function make_coq { make_ocaml make_num make_findlib - # make_camlp5 make_lablgtk if case $COQ_VERSION in @@ -1437,11 +1381,12 @@ function make_coq { log2 make install log1 copy_coq_dlls + log1 copy_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 index 2c8c46373f..2c8c46373f 100755..100644 --- a/dev/build/windows/patches_coq/VST.patch +++ b/dev/build/windows/patches_coq/VST.patch 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-3.0.beta5.patch index 23c303135d..1c6a038da9 100644 --- a/dev/build/windows/patches_coq/lablgtk-2.18.6.patch +++ b/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch @@ -1,33 +1,12 @@ -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 +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-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 +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 @@ -37,22 +16,18 @@ ORIGFOLDER= lablgtk-2.18.3.orig 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 +--- 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> @@ -74,7 +49,7 @@ ORIGFOLDER= lablgtk-2.18.3.orig #include "wrappers.h" #include "ml_glib.h" #include "glib_tags.h" -@@ -325,14 +332,23 @@ +@@ -326,14 +333,23 @@ #ifndef _WIN32 ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref) 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); +} diff --git a/dev/build/windows/patches_coq/quickchick.patch b/dev/build/windows/patches_coq/quickchick.patch index 1afa6e7f95..1afa6e7f95 100755..100644 --- a/dev/build/windows/patches_coq/quickchick.patch +++ b/dev/build/windows/patches_coq/quickchick.patch diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index ac763547b6..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) - libgtk2.0-dev libgtksourceview2.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="lablgtk.2.18.5 conf-gtksourceview.2" +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="lablgtk.2.18.6 conf-gtksourceview.2" \ + 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/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 8420d930d5..0f3fd38a7a 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 @@ -55,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 @@ -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 @@ -279,10 +278,10 @@ 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 (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 +291,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 +310,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 +330,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 +354,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 +370,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 +384,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 +411,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 +451,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. *) @@ -493,9 +466,9 @@ 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) (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 @@ -520,9 +493,10 @@ class ['a] list_param_box (param : 'a list_param) (tt:GData.tooltips) = param.list_f_apply !listref ; param.list_value <- !listref 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 +527,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,11 +658,9 @@ 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 + let _ = dialog#vbox#pack ~expand:true config_box#box#coerce in if with_apply then dialog#add_button Configwin_messages.mApply `APPLY; @@ -697,7 +669,6 @@ let edit ?(with_apply=true) dialog#add_button Configwin_messages.mCancel `CANCEL; let destroy () = - tooltips#destroy () ; dialog#destroy (); in let rec iter rep = @@ -714,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 = @@ -744,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) -> ())) @@ -753,7 +727,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 +742,6 @@ let list ?(editable=true) ?help list_f_add = add ; list_f_apply = f ; } - tt ) (** Create a strings param. *) @@ -777,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 -> 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 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/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/coqide.ml b/ide/coqide.ml index 94778e0c60..eaeeaa0001 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 @@ -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" @@ -271,11 +272,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 @@ -359,7 +360,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 @@ -812,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 @@ -939,7 +940,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 @@ -972,7 +973,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; @@ -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 ()); ]; @@ -1220,10 +1222,10 @@ 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 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; @@ -1303,11 +1305,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/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 @@ -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) 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/ideutils.ml b/ide/ideutils.ml index 5beaba3604..8c5b3fcc5b 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; @@ -229,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) ?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 ; - 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 () @@ -255,10 +259,10 @@ let select_file_for_open ~title ?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 531c71cd4b..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 -> ?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 : 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..69dbc0b235 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) @@ -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 *) @@ -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 @@ -575,7 +578,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 +590,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; @@ -691,7 +694,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,19 +706,19 @@ 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:(Tags.color_of_string pref#get) - ~packing:(table#attach ~left:1 ~top:i) () + ~color:(Gdk.Color.color_parse pref#get) + ~packing:(grid#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 () @@ -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 @@ -740,7 +744,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 +754,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 @@ -921,6 +925,7 @@ let configure ?(apply=(fun () -> ())) parent = else cmd_browse#get]) cmd_browse#get in +(* let automatic_tactics = strings ~f:automatic_tactics#set @@ -929,12 +934,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 +971,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 +995,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 diff --git a/ide/preferences.mli b/ide/preferences.mli index cf2265781c..8745c2ae91 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 @@ -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 diff --git a/ide/session.ml b/ide/session.ml index e2427a9b51..fd21515ca5 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) @@ -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 @@ -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. *) diff --git a/ide/tags.ml b/ide/tags.ml index 60195e8acb..e9dbcb9e67 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 = @@ -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..be400a5f2d 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -100,10 +100,10 @@ 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 + 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 () = @@ -163,8 +163,8 @@ object(self) frame#visible method private refresh_color clr = - let clr = Tags.color_of_string clr in - let iter (_,view,_) = view#misc#modify_base [`NORMAL, `COLOR clr] in + let clr = Gdk.Color.color_parse clr in + let iter (_,view,_) = view#misc#modify_bg [`NORMAL, `COLOR clr] in List.iter iter views initializer 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) diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index 7d2d7da570..fe079e8a9e 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 @@ -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 6b09b344b5..7943b099fc 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 @@ -59,10 +59,10 @@ 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 + 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_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 -> diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 9be562d3ed..596df227b7 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -193,21 +193,21 @@ 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 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 + 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 5e26c50797..e95176bf4d 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 @@ -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 @@ -484,24 +484,24 @@ 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; () 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 -> 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 |