Commit a7821947 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make why3ide compatible with GTK3.

parent 9f13a716
......@@ -219,6 +219,7 @@ pvsbin/
/src/tools/why3wc.ml
# /src/ide
/src/ide/gtkcompat.ml
/src/ide/why3_js.byte
/src/ide/why3_js.js
......
......@@ -41,4 +41,4 @@ B plugins/tptp
B plugins/python
B lib/why3
PKG str unix num dynlink @ZIPLIB@ @LABLGTK2PKG@ @META_OCAMLGRAPH@
PKG str unix num dynlink @ZIPLIB@ @LABLGTKPKG@ @META_OCAMLGRAPH@
......@@ -13,6 +13,7 @@ Tools
IDE
* clicking on the status of a failed proof attempt in the proof tree
now generates counterexamples
* added support for GTK3
Version 1.1.1, December 17, 2018
--------------------------------
......
......@@ -723,7 +723,9 @@ xml-validate-local:
ifeq (@enable_ide@,yes)
IDE_FILES = gconfig ide_utils why3ide
IDEGENERATED = src/ide/gtkcompat.ml
IDE_FILES = gtkcompat gconfig ide_utils why3ide
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
......@@ -734,13 +736,15 @@ IDECMX = $(addsuffix .cmx, $(IDEMODULES))
$(IDEDEP): DEPFLAGS += -I src/ide
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide
$(IDEDEP): $(IDEGENERATED)
# build targets
byte: bin/why3ide.byte
opt: bin/why3ide.opt
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
bin/why3ide.opt bin/why3ide.byte: INCLUDES += @LABLGTKINCLUDE@
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += @LABLGTKLIB@
bin/why3ide.byte: BLINKFLAGS += -custom
bin/why3ide.opt: $(WHY3CMXA) src/ide/resetgc.o $(IDECMX)
......@@ -784,8 +788,17 @@ install:: install-ide
install_local:: bin/why3ide
ifeq (@GTKVERSION@,2)
src/ide/gtkcompat.ml: config.status src/ide/gtkcompat2.ml
cp src/ide/gtkcompat2.ml $@
else
src/ide/gtkcompat.ml: config.status src/ide/gtkcompat3.ml
cp src/ide/gtkcompat3.ml $@
endif
GENERATED += $(IDEGENERATED)
endif
###############
# WEBSERV
......
......@@ -522,50 +522,78 @@ else
DIR=$(ocamlfind query lablgtk2)
if test -n "$DIR"; then
echo "ocamlfind found lablgtk2 in $DIR"
LABLGTK2LIB="$DIR"
LABLGTKINCLUDE="-I $DIR"
fi
fi
if test -z "$DIR"; then
LABLGTK2LIB="+lablgtk2"
LABLGTKINCLUDE="-I +lablgtk2"
DIR="$OCAMLLIB/lablgtk2"
AC_CHECK_FILE($DIR/lablgtk.cma,,enable_ide=no)
fi
AC_CHECK_FILE($DIR/gtkButton.cmi,,enable_ide=no)
if test "$enable_ide" = no; then
AC_MSG_WARN([Lib lablgtk2 not found, IDE disabled.])
reason_ide=" (lablgtk2 not found)"
if test "$enable_ide" = yes; then
GTKVERSION=2
else
AC_MSG_WARN([Lib lablgtk2 not found, trying lablgtk3.])
enable_ide=retry
fi
fi
# checking for lablgtk3
if test "$enable_ide" = retry; then
enable_ide=yes
DIR=
if test "$USEOCAMLFIND" = yes; then
DIR=$(ocamlfind query lablgtk3)
if test -n "$DIR"; then
echo "ocamlfind found lablgtk3 in $DIR"
LABLGTKINCLUDE="-I $DIR"
fi
fi
if test -z "$DIR"; then
LABLGTKINCLUDE="-I +lablgtk3"
DIR="$OCAMLLIB/lablgtk3"
AC_CHECK_FILE($DIR/lablgtk.cma,,enable_ide=no)
fi
AC_CHECK_FILE($DIR/gtkButton.cmi,,enable_ide=no)
if test "$enable_ide" = yes; then
GTKVERSION=3
else
AC_MSG_WARN([Lib lablgtk3 not found, IDE disabled.])
reason_ide=" (lablgtk2/3 not found)"
fi
fi
# checking for lablgtksourceview2
# checking for lablgtksourceview
if test "$enable_ide" = yes ; then
DIR=
if test "$USEOCAMLFIND" = yes; then
DIR=$(ocamlfind query lablgtk2.sourceview2)
DIR=$(ocamlfind query lablgtk$GTKVERSION.sourceview$GTKVERSION)
if test -z "$DIR"; then
DIR=$(ocamlfind query lablgtksourceview2)
DIR=$(ocamlfind query lablgtksourceview$GTKVERSION)
fi
if test -n "$DIR";then
echo "ocamlfind found lablgtksourceview2 in $DIR"
LABLGTKSV2LIB="$DIR"
echo "ocamlfind found lablgtksourceview$GTKVERSION in $DIR"
fi
fi
if test -z "$DIR"; then
DIR="$OCAMLLIB/lablgtk2"
AC_CHECK_FILE($DIR/lablgtksourceview2.cma,,enable_ide=no)
DIR="$OCAMLLIB/lablgtk$GTKVERSION"
AC_CHECK_FILE($DIR/lablgtksourceview$GTKVERSION.cma,,enable_ide=no)
fi
AC_CHECK_FILE($DIR/gSourceView2.cmi,,enable_ide=no)
AC_CHECK_FILE($DIR/gSourceView$GTKVERSION.cmi,,enable_ide=no)
if test "$enable_ide" = no; then
AC_MSG_WARN([Lib lablgtksourceview2 not found, IDE disabled.])
reason_ide=" (lablgtksourceview2 not found)"
AC_MSG_WARN([Lib lablgtksourceview not found, IDE disabled.])
reason_ide=" (lablgtksourceview not found)"
fi
fi
if test "$enable_ide" = yes ; then
LABLGTK2PKG="lablgtk2 lablgtk2.init lablgtk2.sourceview2"
LABLGTKLIB="lablgtk lablgtksourceview$GTKVERSION"
LABLGTKPKG="lablgtk$GTKVERSION lablgtk$GTKVERSION.init lablgtk$GTKVERSION.sourceview$GTKVERSION"
else
LABLGTK2PKG=
LABLGTK2LIB=
LABLGTKLIB=
LABLGTKPKG=
LABLGTKINCLUDE=
fi
dnl AC_CHECK_PROG(enable_ide,lablgtk2,yes,no) not always available (Win32)
......@@ -861,8 +889,10 @@ AC_SUBST(MENHIR)
AC_SUBST(enable_profiling)
AC_SUBST(enable_ide)
AC_SUBST(LABLGTK2LIB)
AC_SUBST(LABLGTK2PKG)
AC_SUBST(LABLGTKLIB)
AC_SUBST(LABLGTKPKG)
AC_SUBST(LABLGTKINCLUDE)
AC_SUBST(GTKVERSION)
AC_SUBST(enable_web_ide)
AC_SUBST(enable_js_of_ocaml)
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
#13 "src/ide/gtkcompat2.ml"
module GSourceView = GSourceView2
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
#13 "src/ide/gtkcompat3.ml"
module GSourceView = GSourceView3
......@@ -16,8 +16,7 @@ open Wstdlib
open Ide_utils
open History
open Itp_communication
module GSourceView = GSourceView2
open Gtkcompat
external reset_gc : unit -> unit = "ml_reset_gc"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment