diff options
| -rw-r--r-- | .gitignore | 6 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | Makefile.build | 8 | ||||
| -rwxr-xr-x | configure | 25 | ||||
| -rw-r--r-- | ide/undo.mli (renamed from ide/undo_lablgtk_ge212.mli) | 0 | ||||
| -rw-r--r-- | ide/undo_lablgtk_ge26.mli | 33 | ||||
| -rw-r--r-- | ide/undo_lablgtk_lt26.mli | 33 |
7 files changed, 10 insertions, 97 deletions
diff --git a/.gitignore b/.gitignore index d2e2bcb5c..8c14100cd 100644 --- a/.gitignore +++ b/.gitignore @@ -104,11 +104,6 @@ tools/coqdep_lexer.ml tools/coqdoc/cpretty.ml lib/xml_lexer.ml -# .mly files - -ide/config_parser.ml -ide/config_parser.mli - # .ml4 files g_*.ml @@ -147,7 +142,6 @@ ide/coqide_main_opt.ml # other auto-generated files -ide/undo.mli toplevel/mltop.optml toplevel/mltop.byteml kernel/byterun/coq_jumptbl.h @@ -218,7 +218,7 @@ depclean: find . $(FIND_VCS_CLAUSE) '(' -name '*.d' ')' -print | xargs rm -f cleanconfig: - rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-v7 ide/undo.mli + rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-v7 distclean: clean cleanconfig diff --git a/Makefile.build b/Makefile.build index 086587a9d..559d0f378 100644 --- a/Makefile.build +++ b/Makefile.build @@ -295,14 +295,14 @@ coqide-files: $(IDEFILES) $(COQIDEOPT): $(LINKIDEOPT) | $(COQTOPOPT) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(IDEOPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa\ - gtkThread.cmx str.cmxa $(LINKIDEOPT) + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(IDEOPTFLAGS) -o $@ unix.cmxa threads.cmxa\ + lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx str.cmxa $(LINKIDEOPT) $(STRIP) $@ $(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo\ - str.cma $(COQRUNBYTEFLAGS) $(LINKIDE) + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma\ + lablgtksourceview2.cma gtkThread.cmo str.cma $(COQRUNBYTEFLAGS) $(LINKIDE) $(COQIDE): cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE) @@ -629,14 +629,15 @@ if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then else case $lablgtkdir_spec in no) - if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then + if [ -f "${CAMLLIB}/lablgtk2/gSourceView2.mli" ]; then lablgtkdir=${CAMLLIB}/lablgtk2 - elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then + elif [ -f "${CAMLLIB}/site-lib/lablgtk2/gSourceView2.mli" ]; then lablgtkdir=${CAMLLIB}/site-lib/lablgtk2 fi;; yes) - if [ ! -f "$lablgtkdir/glib.mli" ]; then - echo "Incorrect LablGtk2 library (glib.mli not found)." + if [ ! -f "$lablgtkdir/gSourceView2.mli" ]; then + echo "Incorrect LablGtk2 library (gSourceView2.mli not found)." + echo "Make sure that the GtkSourceView bindings are available." echo "Configuration script failed!" exit 1 fi;; @@ -987,22 +988,6 @@ if test "$coq_debug_flag" = "-g" ; then chmod a-w,a+x $OCAMLDEBUGCOQ fi -#################################################### -# Fixing lablgtk types (before/after 2.6.0) -#################################################### - -if [ ! "$COQIDE" = "no" ]; then - if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then - if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then - cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli - else - cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli - fi - else - cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli - fi -fi - ############################################## # Creation of configuration files ############################################## diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo.mli index d9451fd1a..d9451fd1a 100644 --- a/ide/undo_lablgtk_ge212.mli +++ b/ide/undo.mli diff --git a/ide/undo_lablgtk_ge26.mli b/ide/undo_lablgtk_ge26.mli deleted file mode 100644 index a2eb65bd1..000000000 --- a/ide/undo_lablgtk_ge26.mli +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* 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_lablgtk_lt26.mli b/ide/undo_lablgtk_lt26.mli deleted file mode 100644 index b193007b6..000000000 --- a/ide/undo_lablgtk_lt26.mli +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* 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 - - |