diff options
| -rwxr-xr-x | configure | 19 | ||||
| -rw-r--r-- | ide/undo_lablgtk_ge26.mli | 35 | ||||
| -rw-r--r-- | ide/undo_lablgtk_lt26.mli (renamed from ide/undo.mli) | 2 |
3 files changed, 55 insertions, 1 deletions
@@ -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 |