Détection de la version de lablgtk (type GText.view)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7580 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 55 insertions, 1 deletions

diff --git a/configure b/configure
index f0d134ece9..db73e56c0c 100755
--- a/configure
+++ b/configure
@@ -357,6 +357,11 @@ if test -x "${CAMLLIB}/lablgtk2" ; then
         else
             echo "LablGtk2 found, no native threads: bytecode CoqIde will be available"
 	    COQIDE=byte
+	fi
+	if grep "class view " "${CAMLLIB}/lablgtk2/gText.mli" | grep -q "\[>" ; then
+	    LABLGTKGE26=yes;
+        else
+	    LABLGTKGE26=no
 	fi;
     else
         echo "LablGtk2 found but too old: CoqIde will not be available"
@@ -550,6 +555,20 @@ if [ ! -f $COQTOP/dev/ocamldebug-v7 ] ; then
   ln -s `basename $OCAMLDEBUGCOQ` $COQTOP/dev/ocamldebug-v7
 fi
 
+##################################################
+# Fixing lablgtk types
+####################################################
+
+if [ "$LABLGTKGE26" = "yes" ] ; then
+  cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli;
+else
+  cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
+fi
+
+##################################################
+# The end
+####################################################
+
 echo "If anything in the above is wrong, please restart './configure'"
 echo
 echo "*Warning* To compile the system for a new architecture"
diff --git a/ide/undo_lablgtk_ge26.mli b/ide/undo_lablgtk_ge26.mli
new file mode 100644
index 0000000000..e949daafed
--- /dev/null
+++ b/ide/undo_lablgtk_ge26.mli
@@ -0,0 +1,35 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(* An undoable view class *)
+
+class undoable_view : [> Gtk.text_view] Gtk.obj ->
+object
+  inherit GText.view
+  method undo : bool
+  method redo : bool
+  method clear_undo : unit
+end
+
+val undoable_view : 
+    ?buffer:GText.buffer ->
+    ?editable:bool ->
+    ?cursor_visible:bool ->
+    ?justification:GtkEnums.justification ->
+    ?wrap_mode:GtkEnums.wrap_mode ->
+    ?border_width:int ->
+    ?width:int ->
+    ?height:int ->
+    ?packing:(GObj.widget -> unit) ->
+    ?show:bool ->
+    unit ->
+  undoable_view
+
+
diff --git a/ide/undo.mli b/ide/undo_lablgtk_lt26.mli
index 1ea8fbea09..82bcf2384d 100644
--- a/ide/undo.mli
+++ b/ide/undo_lablgtk_lt26.mli
@@ -10,7 +10,7 @@
 
 (* An undoable view class *)
 
-class undoable_view : [>Gtk.text_view] Gtk.obj ->
+class undoable_view : Gtk.text_view Gtk.obj ->
 object
   inherit GText.view
   method undo : bool