interface GTK2 experimentale

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

15 files changed, 1192 insertions, 85 deletions

diff --git a/.depend b/.depend
index 820d0d7cf..fa1854bb7 100644
--- a/.depend
+++ b/.depend
@@ -1,3 +1,4 @@
+ide/coq.cmi: kernel/names.cmi kernel/term.cmi toplevel/vernacexpr.cmo 
 interp/constrextern.cmi: kernel/environ.cmi library/libnames.cmi \
     kernel/names.cmi library/nametab.cmi pretyping/pattern.cmi \
     pretyping/rawterm.cmi kernel/sign.cmi interp/symbols.cmi kernel/term.cmi \
@@ -38,10 +39,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/univ.cmi 
 kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
-kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi 
 kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi 
+kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi 
 kernel/names.cmi: lib/pp.cmi lib/predicate.cmi 
 kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
@@ -61,9 +62,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/bignat.cmi: lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
-lib/rtree.cmi: lib/pp.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \
     kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \
     kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \
@@ -93,6 +91,9 @@ library/nameops.cmi: kernel/names.cmi lib/pp.cmi
 library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi lib/util.cmi 
 library/summary.cmi: library/libnames.cmi kernel/names.cmi 
+lib/rtree.cmi: lib/pp.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \
     library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \
     lib/util.cmi 
@@ -304,20 +305,20 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
-toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
     library/libnames.cmi kernel/names.cmi kernel/term.cmi \
     interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: proofs/tacexpr.cmo 
+toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi 
 contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi 
 contrib/correctness/past.cmi: kernel/names.cmi contrib/correctness/ptype.cmi \
     kernel/term.cmi interp/topconstr.cmi lib/util.cmi 
-contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
-    pretyping/rawterm.cmi 
 contrib/correctness/pcicenv.cmi: kernel/names.cmi \
     contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
     kernel/sign.cmi kernel/term.cmi 
+contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
+    pretyping/rawterm.cmi 
 contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \
     contrib/correctness/ptype.cmi 
 contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi 
@@ -427,6 +428,22 @@ dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \
     pretyping/termops.cmx kernel/univ.cmx 
 doc/parse.cmo: parsing/ast.cmi 
 doc/parse.cmx: parsing/ast.cmx 
+ide/coqide.cmo: ide/coq.cmi ide/find_phrase.cmo ide/highlight.cmo \
+    lib/pp_control.cmi toplevel/vernacexpr.cmo 
+ide/coqide.cmx: ide/coq.cmx ide/find_phrase.cmx ide/highlight.cmx \
+    lib/pp_control.cmx toplevel/vernacexpr.cmx 
+ide/coq.cmo: toplevel/cerrors.cmi toplevel/coqtop.cmi kernel/environ.cmi \
+    pretyping/evarutil.cmi pretyping/evd.cmi kernel/names.cmi lib/options.cmi \
+    parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \
+    proofs/proof_trees.cmi proofs/refiner.cmi proofs/tacmach.cmi \
+    kernel/term.cmi lib/util.cmi toplevel/vernac.cmi toplevel/vernacexpr.cmo \
+    ide/coq.cmi 
+ide/coq.cmx: toplevel/cerrors.cmx toplevel/coqtop.cmx kernel/environ.cmx \
+    pretyping/evarutil.cmx pretyping/evd.cmx kernel/names.cmx lib/options.cmx \
+    parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \
+    proofs/proof_trees.cmx proofs/refiner.cmx proofs/tacmach.cmx \
+    kernel/term.cmx lib/util.cmx toplevel/vernac.cmx toplevel/vernacexpr.cmx \
+    ide/coq.cmi 
 interp/constrextern.cmo: pretyping/classops.cmi library/declare.cmi \
     pretyping/detyping.cmi kernel/environ.cmi library/impargs.cmi \
     kernel/inductive.cmi library/libnames.cmi library/nameops.cmi \
@@ -551,6 +568,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
 kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
     kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi 
+kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+    kernel/univ.cmi lib/util.cmi kernel/modops.cmi 
+kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
+    kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+    kernel/univ.cmx lib/util.cmx kernel/modops.cmi 
 kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
     kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
@@ -559,12 +582,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
     kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
     kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
     kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi 
-kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
-    kernel/univ.cmi lib/util.cmi kernel/modops.cmi 
-kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
-    kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
-    kernel/univ.cmx lib/util.cmx kernel/modops.cmi 
 kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \
     kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \
@@ -647,34 +664,24 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
 lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi 
 lib/explore.cmo: lib/explore.cmi 
 lib/explore.cmx: lib/explore.cmi 
-lib/gmap.cmo: lib/gmap.cmi 
-lib/gmap.cmx: lib/gmap.cmi 
 lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
 lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
+lib/gmap.cmo: lib/gmap.cmi 
+lib/gmap.cmx: lib/gmap.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
-lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
-lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/pp_control.cmo: lib/pp_control.cmi 
 lib/pp_control.cmx: lib/pp_control.cmi 
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/predicate.cmo: lib/predicate.cmi 
 lib/predicate.cmx: lib/predicate.cmi 
 lib/profile.cmo: lib/profile.cmi 
 lib/profile.cmx: lib/profile.cmi 
-lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi 
-lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/util.cmi 
 library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \
     library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \
     library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
@@ -779,6 +786,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
     lib/system.cmx library/states.cmi 
 library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi 
+lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi 
+lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/util.cmi 
 parsing/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \
     parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
     toplevel/vernacexpr.cmo 
@@ -1789,10 +1806,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
     pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
     tactics/wcclausenv.cmi 
-tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
-tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
 tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
 tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
+tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
 tools/gallina.cmo: tools/gallina_lexer.cmo 
 tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
@@ -1995,16 +2012,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \
     toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi 
 toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi 
-toplevel/vernac.cmo: parsing/coqast.cmi library/lib.cmi library/library.cmi \
-    kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
-    lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \
-    toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
-    toplevel/vernacinterp.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/coqast.cmx library/lib.cmx library/library.cmx \
-    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
-    lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \
-    toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
-    toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \
     pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \
     interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \
@@ -2065,6 +2072,16 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \
     kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \
     proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi 
+toplevel/vernac.cmo: parsing/coqast.cmi library/lib.cmi library/library.cmi \
+    kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \
+    toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: parsing/coqast.cmx library/lib.cmx library/library.cmx \
+    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
+    lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \
+    toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi contrib/cc/ccalgo.cmi 
 contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx contrib/cc/ccalgo.cmi 
 contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi \
@@ -2085,6 +2102,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
     lib/pp.cmx parsing/pptactic.cmx proofs/proof_type.cmx proofs/refiner.cmx \
     tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
+contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
+    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
 contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \
     pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \
     kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \
@@ -2101,18 +2130,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \
     kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
     interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi 
-contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
-    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
-    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
-contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
-    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
-    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
 contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \
     kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
     contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -2653,6 +2670,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \
     tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx interp/topconstr.cmx \
     pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi 
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+    parsing/printer.cmi contrib/interface/translate.cmi \
+    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+    parsing/printer.cmx contrib/interface/translate.cmx \
+    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/showproof.cmo: proofs/clenv.cmi interp/constrintern.cmi \
     parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \
     pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -2677,14 +2702,6 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.cmx \
     pretyping/termops.cmx contrib/interface/translate.cmx \
     pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/interface/showproof.cmi 
-contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
-    parsing/printer.cmi contrib/interface/translate.cmi \
-    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
-contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
-    parsing/printer.cmx contrib/interface/translate.cmx \
-    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     interp/constrextern.cmi contrib/interface/ctast.cmo kernel/environ.cmi \
     pretyping/evarutil.cmi pretyping/evd.cmi library/libobject.cmi \
@@ -2857,12 +2874,12 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
     proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx lib/util.cmx 
-contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi 
-contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx 
 contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \
     kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi 
 contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \
     kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx 
+contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi 
+contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx 
 contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo library/declare.cmi \
     library/dischargedhypsmap.cmi contrib/xml/doubleTypeInference.cmi \
     kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
@@ -2917,8 +2934,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \
     contrib/xml/xml.cmx 
 contrib/xml/unshare.cmo: contrib/xml/unshare.cmi 
 contrib/xml/unshare.cmx: contrib/xml/unshare.cmi 
-contrib/xml/xml.cmo: contrib/xml/xml.cmi 
-contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 contrib/xml/xmlcommand.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \
     contrib/xml/cic2acic.cmo library/decl_kinds.cmo kernel/declarations.cmi \
     library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
@@ -2945,6 +2960,8 @@ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
     parsing/pptactic.cmx tactics/tacinterp.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx 
+contrib/xml/xml.cmo: contrib/xml/xml.cmi 
+contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 tactics/tauto.cmo: parsing/grammar.cma
 tactics/tauto.cmx: parsing/grammar.cma
 tactics/newtauto.cmo: parsing/grammar.cma
diff --git a/Makefile b/Makefile
index c5f1077ac..f15da41ff 100644
--- a/Makefile
+++ b/Makefile
@@ -39,7 +39,7 @@ noargument:
 
 LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
               -I proofs -I tactics -I pretyping \
-              -I interp -I toplevel -I parsing \
+              -I interp -I toplevel -I parsing -I ide \
               -I contrib/omega -I contrib/romega \
 	      -I contrib/ring -I contrib/xml \
 	      -I contrib/extraction -I contrib/correctness \
@@ -413,6 +413,34 @@ scripts/tolink.ml: Makefile
 
 beforedepend:: scripts/tolink.ml
 
+# Coq IDE
+
+COQIDEBYTE=bin/coqide.byte$(EXE)
+COQIDEOPT=bin/coqide.opt$(EXE)
+COQIDECMO=ide/find_phrase.cmo ide/highlight.cmo ide/coq.cmo ide/coqide.cmo
+COQIDECMX=$(COQIDECMO:.cmo=.cmx)
+COQIDEFLAGS=-I +lablgtk2
+beforedepend:: ide/find_phrase.ml ide/highlight.ml
+
+$(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQIDECMX)
+	$(COQMKTOP) -ide -opt $(COQIDEFLAGS) lablgtk.cmxa $(OPTFLAGS) -o $@ $(COQIDECMX)
+	$(STRIP) $@
+
+$(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(COQIDECMO)
+	$(COQMKTOP) -g -ide -top $(COQIDEFLAGS) lablgtk.cma $(LOCALINCLUDES) $(CAMLDEBUG) -o $@ $(COQIDECMO)
+
+ide/%.cmo: ide/%.ml
+	$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+
+ide/%.cmi: ide/%.mli
+	$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
+
+ide/%.cmx: ide/%.ml
+	$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
+
+clean::
+	rm -f $(COQIDEBYTE) $(COQIDEOPT)
+
 # coqc
 
 COQCCMO=$(CONFIG) toplevel/usage.cmo scripts/coqc.cmo
@@ -1094,6 +1122,7 @@ archclean::
 	rm -f parsing/*.cmx parsing/*.[so]
 	rm -f pretyping/*.cmx pretyping/*.[so]
 	rm -f toplevel/*.cmx toplevel/*.[so]
+	rm -f ide/*.cmx ide/*.[so]
 	rm -f tools/*.cmx tools/*.[so]
 	rm -f scripts/*.cmx scripts/*.[so]
 	rm -f dev/*.cmx dev/*.[so]
@@ -1111,6 +1140,7 @@ clean:: archclean
 	rm -f parsing/*.cm[io] parsing/*.ppo
 	rm -f pretyping/*.cm[io]
 	rm -f toplevel/*.cm[io]
+	rm -f ide/*.cm[io]
 	rm -f tools/*.cm[io]
 	rm -f scripts/*.cm[io]
 	rm -f dev/*.cm[io]
diff --git a/bin/.cvsignore b/bin/.cvsignore
index 2a6c2720c..95b4ec7f8 100644
--- a/bin/.cvsignore
+++ b/bin/.cvsignore
@@ -12,3 +12,5 @@ coq-interface
 parser
 coq_vo2xml
 coq-interface.opt
+coqide.byte
+coqide.opt
diff --git a/ide/.cvsignore b/ide/.cvsignore
new file mode 100644
index 000000000..98975db80
--- /dev/null
+++ b/ide/.cvsignore
@@ -0,0 +1,5 @@
+lexer.ml
+why_viewer
+.depend
+find_phrase.ml
+highlight.ml
diff --git a/ide/coq.ml b/ide/coq.ml
new file mode 100644
index 000000000..9dde20439
--- /dev/null
+++ b/ide/coq.ml
@@ -0,0 +1,156 @@
+open Vernac
+open Vernacexpr
+open Pfedit
+open Pp
+open Util
+open Names
+open Term
+open Printer
+open Environ
+open Evarutil
+open Evd
+
+
+let output = ref (Format.formatter_of_out_channel stdout)
+
+let msg x = 
+  Format.fprintf !output "%s\n" x;
+  Format.pp_print_flush !output ();;
+ 
+let init () = 
+  Options.make_silent true;
+  Coqtop.init ()
+
+let i = ref 0
+
+let interp s = 
+  prerr_endline s;
+  flush stderr;
+  let po = Pcoq.Gram.parsable (Stream.of_string s) in
+  Vernac.raw_do_vernac po;
+  let po = Pcoq.Gram.parsable (Stream.of_string s) in
+  match Pcoq.Gram.Entry.parse Pcoq.main_entry po with
+    (* | Some (_, VernacDefinition _) *)
+    | Some (_,ast) -> 
+	prerr_endline ("Done with "^s);
+	flush stderr;
+	ast
+    | None -> assert false
+
+let msg m = 
+  let b =  Buffer.create 103 in
+  Pp.msg_with (Format.formatter_of_buffer b) m;
+  Buffer.contents b
+
+let msgnl m = 
+  (msg m)^"\n"
+
+let rec is_pervasive_exn = function
+  | Out_of_memory | Stack_overflow | Sys.Break -> true
+  | Error_in_file (_,_,e) -> is_pervasive_exn e
+  | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
+  | DuringCommandInterp (_,e) -> is_pervasive_exn e
+  | _ -> false
+
+let print_toplevel_error exc =
+  let (dloc,exc) =
+    match exc with
+      | DuringCommandInterp (loc,ie) ->
+          if loc = dummy_loc then (None,ie) else (Some loc, ie)
+      | _ -> (None, exc) 
+  in
+  let (loc,exc) =
+    match exc with
+      | Stdpp.Exc_located (loc, ie) -> (Some loc),ie
+      | Error_in_file (s, (fname, loc), ie) -> assert false
+      | _ -> dloc,exc
+  in
+  match exc with
+    | End_of_input  -> 	str "Please report: End of input",None
+    | Vernacexpr.ProtectedLoop -> 
+	str "ProtectedLoop  not allowed by coqide!",None
+    | Vernacexpr.Drop ->  str "Drop is not allowed by coqide!",None
+    | Vernacexpr.Quit -> str "Quit is not allowed by coqide! Use menus.",None
+    | _ -> 
+	(Cerrors.explain_exn exc),
+	(if is_pervasive_exn exc then None else loc)
+
+let process_exn e = let s,loc=print_toplevel_error e in (msgnl s,loc)
+
+(* type hyp = (identifier * constr option * constr) * string*)
+type hyp = ((identifier * string) * constr option * constr) * (string * string)
+type concl = constr * string
+type goal = hyp list * concl
+
+let prepare_hyp env ((i,c,d) as a) =
+  ((i,string_of_id i),c,d), (msg (pr_var_decl env a), 
+			     msg (prterm_env_at_top env d))
+
+let prepare_hyps env =
+  assert (rel_context env = []);
+  let hyps =
+    fold_named_context
+      (fun env d acc -> let hyp =  prepare_hyp env d in hyp :: acc)
+      env ~init:[] 
+  in
+  List.rev hyps
+
+let prepare_goal g =
+  let env = evar_env g in
+  (prepare_hyps env,
+   (g.evar_concl, msg (prterm_env_at_top env g.evar_concl)))
+
+let get_curent_goals () = 
+    let pfts = get_pftreestate () in
+    let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in 
+    List.map prepare_goal gls
+
+let print_no_goal () =
+    let pfts = get_pftreestate () in
+    let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in 
+    assert (gls = []);
+    let sigma = Tacmach.project (Tacmach.top_goal_of_pftreestate pfts) in
+    msg (Proof_trees.pr_subgoals_existential sigma gls)
+
+
+type word_class = Normal | Kwd | Reserved
+
+
+let kwd = [(* "Compile";"Inductive";"Qed";"Type";"end";"Axiom";
+	      "Definition";"Load";"Quit";"Variable";"in";"Cases";"FixPoint";
+	      "Parameter";"Set";"of";"CoFixpoint";"Grammar";"Proof";"Syntax";
+	      "using";"CoInductive";"Hypothesis";"Prop";"Theorem";
+	   *)
+  "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
+  "CoInductive"; "Defined"; "Definition"; 
+  "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint";
+  "Hints"; "Hypothesis"; "Immediate"; "Implicits"; "Import"; "Inductive"; 
+  "Infix"; "Lemma"; "Load"; "Local"; 
+  "Match"; "Module"; "Module Type";
+  "Mutual"; "Parameter"; "Print"; "Proof"; "Qed";
+  "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
+  "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
+  "Unset"; "Variable"; "Variables"; 
+]
+	    
+let reserved = []
+
+module SHashtbl = 
+  Hashtbl.Make 
+    (struct 
+       type t = string
+       let equal = ( = )
+       let hash = Hashtbl.hash
+     end)
+
+
+let word_tbl = SHashtbl.create 37
+let _ = 
+  List.iter (fun w -> SHashtbl.add word_tbl w Kwd) kwd;
+  List.iter (fun w -> SHashtbl.add word_tbl w Reserved) reserved
+
+let word_class s = 
+  try
+    SHashtbl.find word_tbl s
+  with Not_found -> Normal
+
diff --git a/ide/coq.mli b/ide/coq.mli
new file mode 100644
index 000000000..3e81c1196
--- /dev/null
+++ b/ide/coq.mli
@@ -0,0 +1,22 @@
+open Names
+open Term
+
+
+val init : unit -> unit 
+val interp : string -> Vernacexpr.vernac_expr
+
+(* type hyp = (identifier * constr option * constr) * string *)
+
+type hyp = ((identifier*string) * constr option * constr) * (string * string)
+type concl = constr * string
+type goal = hyp list * concl
+
+val get_curent_goals : unit -> goal list
+
+val print_no_goal : unit -> string
+
+val process_exn : exn -> string*((int*int) option)
+
+type word_class = Normal | Kwd | Reserved
+
+val word_class : string -> word_class
diff --git a/ide/coqide.ml b/ide/coqide.ml
new file mode 100644
index 000000000..b6ea38709
--- /dev/null
+++ b/ide/coqide.ml
@@ -0,0 +1,763 @@
+let window_width = 1280
+let window_height = 1024
+
+
+let monospace_font = ref (Pango.Font.from_string "Courier bold 14")
+let general_font = ref !monospace_font
+let lower_view_general_font = ref (Pango.Font.from_string "Courier bold 14")
+let upper_view_general_font = ref !general_font
+let statusbar_font = ref !general_font
+let proved_lemma_font = ref !monospace_font
+let to_prove_lemma_font = ref !monospace_font
+let discharged_lemma_font = ref !monospace_font
+
+let (load_m:GMenu.menu_item option ref) = ref None
+let (save_m:GMenu.menu_item option ref) = ref None
+let (rehighlight_m:GMenu.menu_item option ref) = ref None
+let (refresh_m:GMenu.menu_item option ref) = ref None
+let last_filename = ref None
+
+let status = ref None
+let push_info = ref (function s -> failwith "not ready")
+let pop_info = ref (function s -> failwith "not ready")
+let flash_info = ref  (function s -> failwith "not ready")
+
+let out_some s = match s with | None -> assert false | Some f -> f
+
+let try_convert s = 
+  try
+    if Glib.Utf8.validate s then s else
+      (prerr_endline 
+	 "Coqide warning: input is not UTF-8 encoded. Trying to convert from locale.";
+       Glib.Convert.locale_to_utf8 s)
+  with _ -> 
+    "(* Fatal error: wrong encoding in input.
+Please set your locale according to your file encoding.*)"
+
+let try_export file_name s = 
+  try 
+    let s = Glib.Convert.locale_from_utf8 s in
+    let oc = open_out file_name in
+    output_string oc s;
+    close_out oc
+  with e -> prerr_endline (Printexc.to_string e)
+
+let input_channel b ic =
+  let buf = String.create 1024 and len = ref 0 in
+  while len := input ic buf 0 1024; !len > 0 do
+    Buffer.add_substring b buf 0 !len
+  done
+
+let with_file name ~f =
+  let ic = open_in name in
+  try f ic; close_in ic with exn -> close_in ic; raise exn
+
+type info =  {start:GText.mark;
+	      stop:GText.mark;
+	      ast:Vernacexpr.vernac_expr}
+exception Size of int
+let (processed_stack:info Stack.t) = Stack.create ()
+let push x = Stack.push x processed_stack
+let pop () = try Stack.pop processed_stack with Stack.Empty -> raise (Size 0)
+let top () = try Stack.top processed_stack with Stack.Empty -> raise (Size 0)
+let top_top () =
+    let first = pop () in
+    let snd = try top () with Size 0 -> push first; raise (Size 1) in
+    push first;
+   snd
+
+(* For electric handlers *)
+exception Found
+
+(* For find_phrase_starting_at *)
+exception Stop of int
+
+let set_break () = 
+  Sys.set_signal Sys.sigusr1 (Sys.Signal_handle (fun _ -> raise Sys.Break))
+let unset_break () = 
+  Sys.set_signal Sys.sigusr1 Sys.Signal_ignore
+
+let pid = Unix.getpid ()
+
+let break () = Unix.kill pid Sys.sigusr1
+let can_break () = set_break () 
+(* ignore (Unix.sigprocmask Unix.SIG_UNBLOCK [Sys.sigusr1])*) 
+let cant_break () = unset_break () 
+(* ignore (Unix.sigprocmask Unix.SIG_BLOCK [Sys.sigusr1])*)
+
+
+(* Get back the standard coq out channels *)
+let read_stdout,clear_stdout =
+  let out_buff = Buffer.create 100 in
+  Pp_control.std_ft := Format.formatter_of_buffer out_buff;
+  (fun () -> Format.pp_print_flush !Pp_control.std_ft (); 
+     let r = Buffer.contents out_buff in
+     Buffer.clear out_buff; r),
+  (fun () -> 
+     Format.pp_print_flush !Pp_control.std_ft (); Buffer.clear out_buff)
+
+let process_pending () = 
+  while Glib.Main.pending () do 
+    ignore (Glib.Main.iteration false) 
+  done
+
+let find_tag_limits (tag :GText.tag) (it:GText.iter) = 
+  let start_it = it#copy in
+    if not (start_it#begins_tag ~tag ()) 
+    then ignore (start_it#backward_to_tag_toggle ~tag ());
+    let end_it = it#copy in
+      if not (end_it#ends_tag ~tag ())
+      then ignore (end_it#forward_to_tag_toggle ~tag ());
+      start_it,end_it
+
+let analyze_all 
+  (input_view:GText.view) 
+  (proof_view:GText.view) 
+  (message_view:GText.view)
+  =
+  let input_buffer = input_view#get_buffer in
+  let proof_buffer = proof_view#get_buffer in
+  let message_buffer = message_view#get_buffer in
+  let insert_message s =
+    message_buffer#insert s;
+    message_view#misc#draw None
+  in
+  let set_message s =
+    message_buffer#set_text s;
+    message_view#misc#draw None
+  in
+  let clear_message () =
+    message_buffer#set_text ""
+  in
+  ignore (message_view#get_buffer#connect#after#insert_text
+	    ~callback:(fun it s -> ignore (message_view#scroll_to_mark
+					     ~within_margin:0.49
+					     (message_buffer#get_insert))));
+  let last_index = ref true in
+  let last_array = [|"";""|] in
+  let get_start_of_input () = 
+    input_buffer#get_iter_at_mark 
+      (input_buffer#get_mark ~name:"start_of_input") 
+  in
+  ignore (input_buffer#connect#changed
+	    ~callback:(fun () -> 
+			 input_buffer#remove_tag_by_name 
+			 ~start:(get_start_of_input())
+			 ~stop:input_buffer#get_end_iter
+			 "error"));
+
+  let get_insert () = input_buffer#get_iter_at_mark (input_buffer#get_insert) in
+  let highlight_slice start stop = 
+    let offset = start#get_offset in
+    let s = Glib.Convert.locale_from_utf8 (input_buffer#get_slice ~start ~stop ()) in
+    let lb = Lexing.from_string s in
+    try 
+      while true do
+	process_pending ();
+	let b,e,o=Highlight.next_order lb in
+	let start = input_buffer#get_iter_at ~char_offset:(offset + b) () in
+	let stop = input_buffer#get_iter_at ~char_offset:(offset + e) () in
+	input_buffer#apply_tag_by_name ~start ~stop o 
+      done
+    with End_of_file -> ()
+      | _ -> ()
+  in    
+  let highlight_current_line () = 
+    let i = get_insert () in
+    ignore (i#set_line_offset 0);
+    highlight_slice i (get_insert ())
+  in
+  let highlight_all () = 
+    highlight_slice input_buffer#get_start_iter input_buffer#get_end_iter in      
+  let rec show_goals () = 
+    proof_view#get_buffer#set_text "";
+    let s = Coq.get_curent_goals () in
+    let last_shown_area = proof_buffer#create_tag
+			    ~properties:[`BACKGROUND "light blue"]
+			    ()
+    in
+    match s with 
+      | [] -> proof_buffer#insert (Coq.print_no_goal ())
+      | (hyps,(_,concl))::r -> 
+	  let goal_nb = List.length s in
+	  proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" 
+				 goal_nb
+				 (if goal_nb<=1 then "" else "s"));
+	  List.iter 
+	    (fun (((coqident,ident),_,ast),(s,pr_ast)) -> 
+	       let tag = proof_buffer#create_tag ()
+	       in 
+	       ignore
+		 (tag#connect#event
+		    ~callback:
+		    (fun ~origin ev it ->
+		       match GdkEvent.get_type ev with 
+			 | `BUTTON_PRESS -> 
+			     let ev = (GdkEvent.Button.cast ev) in
+			     if (GdkEvent.Button.button ev) = 3 
+			     then begin 
+			       let loc_menu = GMenu.menu () in
+			       let factory = new GMenu.factory loc_menu in
+			       let add_coq_command cp ip = 
+				 ignore (factory#add_item cp 
+					   ~callback:
+					   (fun () -> ignore
+					      (insert_this_phrase_on_success 
+						 true 
+						 false 
+						 (ip^"\n") 
+						 (ip^"\n"))
+					   )
+					)
+			       in
+			       add_coq_command 
+				 ("Clear "^ident^".")  
+				 ("Clear "^ident^".");
+			       add_coq_command 
+				 ("Elim "^ident^".")
+				 ("Elim "^ident^".");
+			       add_coq_command 
+				 ("Apply "^ident^".")
+				 ("Apply "^ident^".");
+			       add_coq_command 
+				 ("Generalize "^ident^".")
+				 ("Generalize "^ident^".");
+			       add_coq_command 
+				 ("Assumption.")
+				 ("Assumption.");
+			       add_coq_command	
+				 ("Absurd <"^ident^">")
+				 ("Absurd "^
+				  pr_ast
+				  ^".");
+			       add_coq_command 
+				 ("Discriminate "^ident^".")
+				 ("Discriminate "^ident^".");
+			       add_coq_command 
+				 ("Injection "^ident^".")
+				 ("Injection "^ident^".");
+			       add_coq_command 
+				 ("Rewrite "^ident^".")
+				 ("Rewrite "^ident^".");
+			       add_coq_command 
+				 ("Rewrite <- "^ident^".")
+				 ("Rewrite <- "^ident^".");
+			       add_coq_command 
+				 ("Inversion "^ident^".")
+				 ("Inversion "^ident^".");
+			       add_coq_command 
+				 ("Inversion_clear "^ident^".")
+				 ("Inversion_clear "^ident^".");
+			       loc_menu#popup 
+				 ~button:3
+				 ~time:(GdkEvent.Button.time ev);
+			     end
+			 | `MOTION_NOTIFY -> 
+			     proof_buffer#remove_tag
+			     ~start:proof_buffer#get_start_iter
+			     ~stop:proof_buffer#get_end_iter
+			     last_shown_area;
+			     let s,e = find_tag_limits tag 
+					 (new GText.iter it) 
+			     in
+			     proof_buffer#apply_tag 
+			       ~start:s 
+			       ~stop:e 
+			       last_shown_area;
+			     ()
+			 | _ -> ())
+		 );
+	       proof_buffer#insert ~tags:[tag] (s^"\n"))
+	    hyps;
+	  proof_buffer#insert ("--------------------------------------(1/"^
+			       (string_of_int goal_nb)^
+			       ")\n") 
+	    ;
+	  proof_buffer#insert concl;
+	  proof_buffer#insert "\n";
+	  let my_mark = proof_buffer#get_mark ~name:"end_of_conclusion" in
+	  proof_buffer#move_mark
+	    ~where:((proof_buffer#get_iter_at_mark proof_buffer#get_insert))
+	    my_mark;
+	  proof_buffer#insert "\n\n";
+	  let i = ref 1 in
+	  List.iter 
+	    (function (_,(_,concl)) -> 
+	       incr i;
+	       proof_buffer#insert ("----------------------------------------("^
+				    (string_of_int !i)^
+				    "/"^
+				    (string_of_int goal_nb)^
+				    ")\n");
+	       proof_buffer#insert concl;
+	       proof_buffer#insert "\n\n";
+	    )
+	    r;
+	  ignore (proof_view#scroll_to_mark my_mark)
+  and send_to_coq phrase show_error localize = 
+    try
+      !push_info "Coq is computing";
+      (out_some !status)#misc#draw None;
+      input_view#set_editable false;
+      can_break ();
+      let r = Some (Coq.interp phrase) in
+      cant_break ();
+      input_view#set_editable true;
+      !pop_info ();
+      (out_some !status)#misc#draw None;
+      insert_message (read_stdout ());
+      r
+    with e ->
+      input_view#set_editable true;
+      !pop_info ();
+      (if show_error then
+	 let (s,loc) = Coq.process_exn e in
+	 assert (Glib.Utf8.validate s);
+	 set_message s;
+	 message_view#misc#draw None;
+	 if localize then 
+	   (match loc with 
+	      | None -> ()
+	      | Some (start,stop) -> 
+		  let i = get_start_of_input() in 
+		  let starti = i#copy in
+		  ignore (starti#forward_chars start);
+		  let stopi = i#copy in
+		  ignore (stopi#forward_chars stop);
+		  input_buffer#apply_tag_by_name "error"
+   		    ~start:starti
+		    ~stop:stopi
+	   ));
+      None
+  and find_phrase_starting_at (start:GText.iter) = 
+    let end_iter = start#copy in
+    let lexbuf_function s count =
+      try for i = 0 to (count-1) do
+	let c = end_iter#get_char in
+	if c='\000' then raise (Stop 0);
+	s.[i] <- c;	
+	if not (end_iter#forward_char ()) then 
+	  raise (Stop (i+1))
+      done;
+	count
+      with Stop x -> x
+    in
+    try
+      Find_phrase.length := 0;
+      let phrase = Find_phrase.next_phrase (Lexing.from_function lexbuf_function) in
+      end_iter#set_offset (start#get_offset + !Find_phrase.length);
+      Some (start,end_iter)
+    with _ -> None
+  and process_next_phrase display_goals = 
+    clear_message ();
+    match (find_phrase_starting_at (get_start_of_input ()))
+    with None -> false
+      | Some(start,stop) ->
+	  let b = input_buffer in
+	  let phrase = b#get_slice ~start ~stop () in
+	  match send_to_coq phrase true true with
+	    | Some ast ->
+		begin
+		  b#move_mark_by_name ~where:stop "start_of_input";
+		  b#apply_tag_by_name "processed" ~start ~stop;
+		  if ((get_insert())#compare) stop <= 0 then 
+		    (b#place_cursor stop;
+		     ignore (input_view#scroll_to_iter 
+			       ~within_margin:0.2 (get_insert())));
+		  let start_of_phrase_mark = b#create_mark start in
+		  let end_of_phrase_mark = b#create_mark stop in
+		  push
+		    {start = start_of_phrase_mark;
+		     stop = end_of_phrase_mark;
+		     ast= ast};
+		  if display_goals then
+		    (try show_goals () with e -> ());
+		  true;
+		end
+	    | None -> false
+  and insert_this_phrase_on_success show_msg localize coqphrase insertphrase = 
+    match send_to_coq coqphrase show_msg localize with
+      | Some ast ->
+	  begin
+	    let stop = get_start_of_input () in
+	    if stop#starts_line then
+	      input_buffer#insert ~iter:stop insertphrase
+	    else input_buffer#insert ~iter:stop ("\n"^insertphrase); 
+	    let start = get_start_of_input () in
+	    input_buffer#move_mark_by_name ~where:stop "start_of_input";
+	    input_buffer#apply_tag_by_name "processed" ~start ~stop;
+	    if ((get_insert())#compare) stop <= 0 then 
+	      input_buffer#place_cursor stop;
+	    let start_of_phrase_mark = input_buffer#create_mark start in
+	    let end_of_phrase_mark = input_buffer#create_mark stop in
+	    push
+	      {start = start_of_phrase_mark;
+	       stop = end_of_phrase_mark;
+	       ast= ast};
+	    (try show_goals () with e -> ());
+	    true
+	  end
+      | None -> insert_message ("Unsuccesfully tried: "^coqphrase);
+	  false
+  in
+  let process_until_iter_or_error stop =
+    let start = (get_start_of_input ())#copy in
+    input_buffer#apply_tag_by_name 
+      ~start
+      ~stop
+      "to_process";
+    while ((stop#compare (get_start_of_input ())>=0) && process_next_phrase false)
+    do () done;
+    (try show_goals () with _ -> ());
+    input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
+
+  in  
+  let process_until_insert_or_error () = 
+    let stop = get_insert () in
+    process_until_iter_or_error stop
+  in  
+  let reset_initial () = 
+    Stack.iter 
+      (function inf -> 
+	 let start = input_buffer#get_iter_at_mark inf.start in
+	 let stop = input_buffer#get_iter_at_mark inf.stop in
+	 input_buffer#move_mark_by_name ~where:start "start_of_input";
+	 input_buffer#remove_tag_by_name "processed" ~start ~stop;
+	 input_buffer#delete_mark inf.start;
+	 input_buffer#delete_mark inf.stop;
+      ) 
+      processed_stack;
+    Stack.clear processed_stack;
+    clear_message ();
+    send_to_coq "\nReset Initial.\n" true true
+  in
+  let undo_last_step () = 
+    try 
+      let come_back_iter = input_buffer#get_iter_at_mark (top_top ()).start in
+      ignore (reset_initial ());
+      (*      message_buffer#insert "(* Replaying to undo *)\n" ();*)
+      process_until_iter_or_error come_back_iter;
+      input_buffer#place_cursor 
+	(input_buffer#get_iter_at_mark 
+	   (input_buffer#get_mark ~name:"start_of_input"));
+      (*      message_buffer#insert "\n(* End of replay *)\n" ();*)
+    with 
+      | Size 0 -> !flash_info "Nothing to Undo"
+      | Size 1 -> ignore (reset_initial ())
+  in
+  let (* TODO *) undo_just_before (i:GText.iter) =
+    while (i#get_marks<>[] && (i#backward_char ())) do () done;
+    ()
+  in
+  let undo_until_pointer () = 
+    undo_just_before 
+      (let win = match input_view#get_window `WIDGET with
+	 | None -> assert false
+	 | Some w -> w
+       in
+       let x,y = Gdk.Window.get_pointer_location win in
+       let b_x,b_y = input_view#window_to_buffer_coords 
+		       ~tag:`WIDGET 
+		       ~x 
+		       ~y 
+       in
+       input_view#get_iter_at_location ~x:b_x ~y:b_y)
+  in
+  let insert_command cp ip = 
+    clear_message ();
+    ignore (insert_this_phrase_on_success false false cp ip) in
+  let insert_commands l = 
+    clear_message ();
+    ignore (List.exists (fun (cp,ip) -> 
+			   insert_this_phrase_on_success false false cp ip) l)
+  in
+  let _ = input_view#event#connect#key_press 
+	    (function k -> 
+	       match GdkEvent.Key.state k with
+		 | [`MOD1] | [`CONTROL;`MOD1] | [`MOD1;`CONTROL]-> 
+		     let k = GdkEvent.Key.keyval k in
+		     if GdkKeysyms._Down=k 
+		     then ignore (process_next_phrase true) 
+		     else if GdkKeysyms._Right=k 
+		     then process_until_insert_or_error () 
+		     else if GdkKeysyms._Left=k 
+		     then (
+		       ignore(reset_initial ());
+		       process_until_insert_or_error ())
+		     else if GdkKeysyms._r=k 
+		     then ignore (reset_initial ())
+		     else if GdkKeysyms._Up=k 
+		     then ignore (undo_last_step ())
+		     else if GdkKeysyms._Return=k
+		     then ignore(
+		       if (input_buffer#insert_interactive "\n") then
+			 begin
+			   let i= get_insert() in
+			   ignore (i#backward_word_start ());
+			   input_buffer#place_cursor i;
+			   process_until_insert_or_error ()
+			 end)
+		     else if GdkKeysyms._a=k 
+		     then insert_command "Progress Auto.\n" "Auto.\n"
+		     else if GdkKeysyms._i=k 
+		     then insert_command "Progress Intuition.\n" "Intuition.\n"
+		     else if GdkKeysyms._t=k 
+		     then insert_command "Progress Trivial.\n"  "Trivial.\n"
+		     else if GdkKeysyms._o=k 
+		     then insert_command "Omega.\n" "Omega.\n"
+		     else if GdkKeysyms._s=k 
+		     then insert_command "Progress Simpl.\n" "Simpl.\n"
+		     else if GdkKeysyms._e=k 
+		     then insert_command 
+		       "Progress EAuto with *.\n" 
+		       "EAuto with *.\n"
+		     else if GdkKeysyms._asterisk=k 
+		     then insert_command 
+		       "Progress Auto with *.\n"
+		       "Auto with *.\n"
+		     else if GdkKeysyms._dollar=k 
+		     then insert_commands 
+		       ["Progress Trivial.\n","Trivial.\n";
+			"Progress Auto.\n","Auto.\n";
+			"Tauto.\n","Tauto.\n";
+			"Omega.\n","Omega.\n";
+			"Progress Auto with *.\n","Auto with *.\n";
+			"Progress EAuto with *.\n","EAuto with *.\n";
+			"Progress Intuition.\n","Intuition.\n";
+		       ];
+		     true 
+		 | [] -> 
+		     let k = GdkEvent.Key.keyval k in
+		     if GdkKeysyms._Return=k
+		     then
+		       highlight_current_line ();
+		     false
+		 | [`CONTROL] -> 
+		     let k = GdkEvent.Key.keyval k in
+		     if GdkKeysyms._c=k
+		     then break ();
+		     false
+		 | l -> false)
+  in
+  ignore
+    ((out_some !load_m)#connect#activate
+       (fun () -> 
+	  match GToolbox.select_file ~title:"Load file" () with 
+	    | None -> ()
+	    | Some f -> 
+		try
+		  let b = Buffer.create 1024 in
+		  with_file f ~f:(input_channel b);
+		  let s = try_convert (Buffer.contents b) 
+		  in
+		  ignore (reset_initial ());
+		  input_buffer#set_text s;
+		  input_buffer#place_cursor input_buffer#get_start_iter;
+		  highlight_all ();
+		  last_filename := Some f;
+		with e -> !flash_info "Load failed"
+       ));
+  ignore
+    ((out_some !save_m)#connect#activate
+       (fun () ->
+
+	  try match !last_filename with 
+	    | None -> 
+		begin match GToolbox.select_file ~title:"Save file" ()
+		with 
+		  | None -> ()
+		  | Some f -> 
+		      try_export f (input_buffer#get_text ());
+		      last_filename := Some f;
+		end
+	    | Some f -> try_export f (input_buffer#get_text ())
+	  with e -> !flash_info "Save failed"
+	    
+       ));
+  ignore
+    ((out_some !rehighlight_m)#connect#activate
+       highlight_all);
+  let electric_handler () = 
+    input_buffer#connect#insert_text ~callback:
+      (fun it x -> 
+	 begin try
+	   if !last_index then begin
+	     last_array.(0)<-x;
+	     if (last_array.(1) ^ last_array.(0) = ".\n") then raise Found
+	   end else begin
+	     last_array.(1)<-x;
+	     if (last_array.(0) ^ last_array.(1) = ".\n") then raise Found
+	   end
+	 with Found -> 
+	   begin
+	     ignore (process_next_phrase true)
+	   end;
+	 end;
+	 last_index := not !last_index;)
+  in
+  ()
+
+let main () = 
+  let w = GWindow.window 
+	    ~allow_grow:true ~allow_shrink:true ~width:window_width ~height:window_height ~title:"CoqIde" ()
+  in
+  w#misc#modify_font !general_font;
+  let accel_group = GtkData.AccelGroup.create () in
+  let _ = w#connect#destroy ~callback:(fun () -> exit 0) in
+  let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
+  let menubar = GMenu.menu_bar ~packing:vbox#pack () in
+  let factory = new GMenu.factory menubar in
+  let accel_group = factory#accel_group in
+  let file_menu = factory#add_submenu "File" in
+  let file_factory = new GMenu.factory file_menu ~accel_group in
+  load_m := Some (file_factory#add_item "Open" ~key:GdkKeysyms._O);
+  save_m := Some (file_factory#add_item "Save" ~key:GdkKeysyms._S);
+  rehighlight_m := Some (file_factory#add_item "Rehighlight" 
+			   ~key:GdkKeysyms._L);
+  refresh_m := Some (file_factory#add_item "Restart all" ~key:GdkKeysyms._R);
+  let quit_m = file_factory#add_item "Quit" ~key:GdkKeysyms._Q
+		 ~callback:(fun () -> exit 0) in
+
+  let configuration_menu = factory#add_submenu "Configuration" in
+  let configuration_factory = new GMenu.factory configuration_menu ~accel_group
+  in
+(*  let show_discharged_m = configuration_factory#add_check_item 
+			    "Show discharged proof" 
+			    ~key:GdkKeysyms._D
+			    ~callback:(fun b -> () (*show_discharged := b*)) 
+  in*)
+  let customize_colors_m =
+    configuration_factory#add_item "Customize colors"
+      ~callback:(fun () -> !flash_info "Not implemented")
+  in
+  let customize_fonts_m = 
+    configuration_factory#add_item "Customize fonts"
+      ~callback:(fun () -> !flash_info "Not implemented")
+  in
+  let hb = GPack.paned `HORIZONTAL  ~border_width:3 ~packing:vbox#add () in
+  let _ = hb#set_position (window_width*6/10 ) in
+  let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT ~packing:hb#add1 () in 
+  let sw1 = GBin.scrolled_window
+	      ~vpolicy:`AUTOMATIC 
+	      ~hpolicy:`AUTOMATIC
+	      ~packing:fr1#add () in
+  let fr2 = GBin.frame ~shadow_type:`ETCHED_OUT ~packing:hb#add2 () in 
+  let hb2 = GPack.paned `VERTICAL  ~border_width:3 ~packing:fr2#add () in
+  hb2#set_position (window_height*7/10);
+  let sw2 = GBin.scrolled_window 
+	      ~vpolicy:`AUTOMATIC 
+	      ~hpolicy:`AUTOMATIC
+	      ~packing:(hb2#add) () in
+  let sw3 = GBin.scrolled_window 
+	      ~vpolicy:`AUTOMATIC 
+	      ~hpolicy:`AUTOMATIC
+	      ~packing:(hb2#add) () in
+  let status_bar = GMisc.statusbar ~packing:vbox#pack () in
+  status_bar#misc#modify_font !statusbar_font ;
+  let status_context = status_bar#new_context "Messages" in
+  ignore (status_context#push "Ready");
+  status := Some status_bar;
+  push_info := (fun s -> ignore (status_context#push s));
+  pop_info := (fun () -> status_context#pop ());
+  flash_info := (fun s -> status_context#flash ~delay:5000 s);
+  let tv2 = GText.view ~packing:(sw2#add) () in
+  let _ = tv2#misc#modify_font !lower_view_general_font in
+  let _ = tv2#set_editable false in
+  let b = GText.buffer () in 
+  let tb2 = tv2#get_buffer in
+  let tv1 = GText.view ~buffer:b ~packing:(sw1#add) () in
+  let _ = tv1#misc#modify_font !upper_view_general_font in
+  let _ = tv1#set_editable true in
+  let tv3 = GText.view ~packing:(sw3#add) () in
+  let _ = tv3#set_wrap_mode `WORD in
+  let _ = tv3#misc#modify_font !lower_view_general_font in
+  let _ = tv3#set_editable false in
+  let _ = GtkBase.Widget.add_events tv2#as_widget [`POINTER_MOTION] in
+  let _ = tv2#event#connect#motion_notify
+	    ~callback:(fun e -> 
+			 let win = match tv2#get_window `WIDGET with
+			   | None -> assert false
+			   | Some w -> w
+			 in
+			 let x,y = Gdk.Window.get_pointer_location win in
+			 let b_x,b_y = tv2#window_to_buffer_coords 
+					 ~tag:`WIDGET 
+					 ~x 
+					 ~y 
+			 in
+			 let it = tv2#get_iter_at_location ~x:b_x ~y:b_y in
+			 let tags = it#get_tags in
+			 List.iter 
+			   ( fun t ->
+			       ignore (GtkText.Tag.event 
+					 t#as_tag
+					 tv2#as_widget
+					 e 
+					 it#as_textiter))
+			   tags;
+			 false)
+  in
+  b#place_cursor ~where:(b#get_start_iter);
+	    (*  let _ =  refresh_m#connect#activate 
+		~callback:(fun () -> analyze_all tv1 tv2 tv3) 
+		in
+	    *)
+	    w#add_accel_group accel_group;
+    (* Remove default pango menu for textviews *)
+    ignore (tv1#event#connect#button_press ~callback:
+	      (fun ev -> GdkEvent.Button.button ev = 3));
+    ignore (tv2#event#connect#button_press ~callback:
+	      (fun ev -> GdkEvent.Button.button ev = 3));
+    ignore (tv3#event#connect#button_press ~callback:
+	      (fun ev -> GdkEvent.Button.button ev = 3));
+    tv1#misc#grab_focus ();
+    tv2#misc#set_can_focus false;
+    tv3#misc#set_can_focus false;
+    ignore (tv1#get_buffer#create_mark 
+	      ~name:"start_of_input" 
+	      tv1#get_buffer#get_start_iter);
+    ignore (tv2#get_buffer#create_mark 
+	      ~name:"end_of_conclusion" 
+	      tv2#get_buffer#get_start_iter);
+    ignore (tv1#get_buffer#create_tag 
+	      ~name:"to_process" 
+	      ~properties:[`BACKGROUND "light green" ;`EDITABLE false] ());
+    ignore (tv1#get_buffer#create_tag 
+	      ~name:"processed" 
+	      ~properties:[`BACKGROUND "green" ;`EDITABLE false] ());
+    ignore (tv1#get_buffer#create_tag 
+	      ~name:"error" 
+	      ~properties:[`UNDERLINE `DOUBLE ; `FOREGROUND "red"] ());
+    ignore (tv1#get_buffer#create_tag 
+	      ~name:"kwd" 
+	      ~properties:[`FOREGROUND "blue"] ());
+    ignore (tv1#get_buffer#create_tag 
+	      ~name:"decl" 
+	      ~properties:[`FOREGROUND "orange red"] ());
+    ignore (tv1#get_buffer#create_tag 
+	      ~name:"comment" 
+	      ~properties:[`FOREGROUND "brown"] ());
+    ignore (tv1#get_buffer#create_tag 
+	      ~name:"reserved" 
+	      ~properties:[`FOREGROUND "dark red"] ());
+    ignore (tv3#get_buffer#create_tag 
+	      ~name:"error" 
+	      ~properties:[`FOREGROUND "red"] ());
+    w#show ();
+    analyze_all tv1 tv2 tv3
+
+let start () = 
+  cant_break ();
+  Coq.init ();
+  ignore (GtkMain.Main.init ());
+  Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
+						      `WARNING;`CRITICAL]
+    (fun ~level msg ->
+         failwith ("Coqide internal error: " ^ msg)
+    );
+  main ();
+  Sys.catch_break true;
+    try 
+      GMain.Main.main ()
+    with 
+    Sys.Break -> prerr_endline "Interrupted." ; ()
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
new file mode 100644
index 000000000..de19db4c3
--- /dev/null
+++ b/ide/find_phrase.mll
@@ -0,0 +1,22 @@
+{
+  exception Lex_error of string
+  let length = ref 0
+}
+
+rule next_phrase = parse
+  | "(*" { incr length; incr length; 
+	   skip_comment lexbuf;
+	   next_phrase lexbuf}
+  | '.'[' ''\n''\t''\r'] {incr length; incr length; Lexing.lexeme lexbuf}
+  | _ 
+      { incr length; 
+	let c = Lexing.lexeme lexbuf in c^(next_phrase lexbuf) 
+      }
+  | eof  { raise (Lex_error "no phrase") }
+and skip_comment = parse
+  | "*)" {incr length; incr length; ()}
+  | "(*" {incr length; incr length; 
+	  skip_comment lexbuf;
+	  skip_comment lexbuf}
+  | _  { incr length; skip_comment lexbuf}
+  | eof  { raise (Lex_error "No closing *)") }
diff --git a/ide/highlight.mll b/ide/highlight.mll
new file mode 100644
index 000000000..5421e183c
--- /dev/null
+++ b/ide/highlight.mll
@@ -0,0 +1,75 @@
+{
+
+  open Lexing
+
+  type color = string
+
+  type highlight_order = int * int * color
+
+  let comment_start = ref 0
+
+  let kwd = [
+  "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
+  "CoInductive";  "Compile"; "Defined"; "Definition"; 
+  "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint";
+  "Hints"; "Hypothesis"; "Immediate"; "Implicits"; "Import"; "Inductive"; 
+  "Infix"; "Lemma"; "Load"; "Local"; 
+  "Match"; "Module"; "Module Type";
+  "Mutual"; "Parameter"; "Print"; "Proof"; "Qed";
+  "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
+  "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
+  "Unset"; "Variable"; "Variables"; 
+  ]
+
+module SHashtbl = 
+  Hashtbl.Make 
+    (struct 
+       type t = string
+       let equal = ( = )
+       let hash = Hashtbl.hash
+     end)
+
+let word_tbl = SHashtbl.create 37
+let _ =  List.iter (fun w -> SHashtbl.add word_tbl w "kwd") kwd
+}
+
+let keyword = 
+  "Add" | "AddPath" | "Chapter" |
+  "CoInductive" |  "Compile" | "Defined" | 
+  "End" | "Export" | "Fact" | "Fix" | "Global" | 
+  "Grammar" | "Hint" |
+  "Hints" | "Immediate" | "Implicits" | "Import" | 
+  "Infix" | "Load" | "Local" | 
+  "Match" | "Module" | "Module Type" |
+  "Mutual" | "Print" | "Proof" | "Qed" |
+  "Record" | "Recursive" | "Require" | "Save" | "Scheme" |
+  "Section" | "Show" | "Syntactic" | "Syntax" | "Tactic" |
+  "Unset"
+
+let space = 
+  [' ' '\010' '\013' '\009' '\012']
+let firstchar = 
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
+let identchar = 
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
+let ident = firstchar identchar*
+
+let declaration = 
+  "Lemma" | "Axiom" | "CoFixpoint" |"Definition"  |
+  "Fixpoint" | "Hypothesis" | 
+  "Inductive" | "Parameter" | "Remark" |  "Theorem" | 
+  "Variable" | "Variables"
+
+rule next_order = parse
+  | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf }
+  | keyword { lexeme_start lexbuf,lexeme_end lexbuf, "kwd" }
+  | declaration space+ ident 
+            { lexeme_start lexbuf, lexeme_end lexbuf, "decl" } 
+  | _    { next_order lexbuf}
+  | eof  { raise End_of_file }
+
+and comment = parse
+  | "*)" { !comment_start,lexeme_end lexbuf,"comment" }
+  | "(*" { ignore (comment lexbuf); comment lexbuf }
+  | _    { comment lexbuf }
+  | eof  { raise End_of_file }
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 2d4c76d91..d13044c9a 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -169,7 +169,7 @@ let pp_dirs ft =
 
 (* pretty print on stdout and stderr *)
 
-let pp_std_dirs = pp_dirs std_ft
+let pp_std_dirs = pp_dirs !std_ft
 let pp_err_dirs = pp_dirs err_ft
 
 let ppcmds x = Ppdir_ppcmds x
@@ -204,19 +204,19 @@ let msg_warning_with ft strm=
 
 
 (* pretty printing functions WITHOUT FLUSH *)
-let pp        = pp_with std_ft
-let ppnl      = ppnl_with std_ft
+let pp        x = pp_with !std_ft x
+let ppnl      x = ppnl_with !std_ft x
 let pperr     = pp_with err_ft
 let pperrnl   = ppnl_with err_ft
 let message s = ppnl (str s)
-let warning   = warning_with std_ft
-let warn      = warn_with std_ft
-let pp_flush  = Format.pp_print_flush std_ft
+let warning   x = warning_with !std_ft x
+let warn      x = warn_with !std_ft x
+let pp_flush  x = Format.pp_print_flush !std_ft x
 let flush_all() = flush stderr; flush stdout; pp_flush()
 
 (* pretty printing functions WITH FLUSH *)
-let msg = msg_with std_ft
-let msgnl = msgnl_with std_ft
+let msg x = msg_with !std_ft x
+let msgnl x = msgnl_with !std_ft x
 let msgerr = msg_with err_ft
 let msgerrnl = msgnl_with err_ft
-let msg_warning = msg_warning_with std_ft
+let msg_warning x = msg_warning_with !std_ft x
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 78b78020d..3b1266c2c 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -86,8 +86,8 @@ let with_output_to ch =
   set_gp ft deep_gp; 
   ft
 
-let std_ft = Format.std_formatter
-let _ = set_dflt_gp std_ft
+let std_ft = ref Format.std_formatter
+let _ = set_dflt_gp !std_ft
 
 let err_ft = with_output_to stderr
 
@@ -95,8 +95,8 @@ let deep_ft = with_output_to stdout
 let _ = set_gp deep_ft deep_gp
 
 (* For parametrization through vernacular *)
-let default = Format.pp_get_max_boxes std_ft ()
-let get_depth_boxes () = Some (Format.pp_get_max_boxes std_ft ())
+let default = Format.pp_get_max_boxes !std_ft ()
+let get_depth_boxes () = Some (Format.pp_get_max_boxes !std_ft ())
 let set_depth_boxes v =
-  Format.pp_set_max_boxes std_ft (match v with None -> default | Some v -> v)
+  Format.pp_set_max_boxes !std_ft (match v with None -> default | Some v -> v)
 
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 548b98a7f..256cc26de 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -36,7 +36,7 @@ val err_fp : (int*string) pp_formatter_params
 val with_fp : 'a pp_formatter_params -> Format.formatter
 val with_output_to : out_channel -> Format.formatter
 
-val std_ft : Format.formatter
+val std_ft : Format.formatter ref
 val err_ft : Format.formatter
 val deep_ft : Format.formatter
 
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 6f65d324b..ad6623328 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -61,6 +61,7 @@ let opt        = ref false
 let full       = ref false
 let top        = ref false
 let searchisos = ref false
+let coqide     = ref false
 let echo       = ref false
 
 let src_dirs = [ []; [ "config" ]; [ "toplevel" ] ]
@@ -138,6 +139,7 @@ Options are:
   -full         Link high level tactics
   -top          Build Coq on a ocaml toplevel (incompatible with -opt)
   -searchisos   Build a toplevel for SearchIsos
+  -ide          Build a toplevel for the Coq IDE
   -R dir        Specify recursively directories for Ocaml\n";
   exit 1
 
@@ -152,6 +154,8 @@ let parse_args () =
     | "-top" :: rem -> top := true ; parse (op,fl) rem
     | "-searchisos" :: rem ->
         searchisos := true; parse (op,fl) rem
+    | "-ide" :: rem ->
+        coqide := true; parse (op,fl) rem
     | "-echo" :: rem -> echo := true ; parse (op,fl) rem
     | ("-cclib"|"-ccopt"|"-I"|"-o" as o) :: rem' ->
 	begin
@@ -259,7 +263,9 @@ let create_tmp_main_file modules =
     (* Start the right toplevel loop: Coq or Coq_searchisos *)
     if !searchisos then 
       output_string oc "Cmd_searchisos_line.start();;\n"
-    else 
+    else if !coqide then
+      output_string oc "Coqide.start();;\n"
+    else
       output_string oc "Coqtop.start();;\n";
     close_out oc;
     main_name
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6c56ca10b..c136507fb 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -215,11 +215,10 @@ let parse_args () =
 (* To prevent from doing the initialization twice *)
 let initialized = ref false
 
-(* Ctrl-C is fatal during the initialisation *)
-let start () =
+let init () =
   if not !initialized then begin
     initialized := true;
-    Sys.catch_break false;
+    Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
     Lib.init();
     try
       parse_args ();
@@ -241,7 +240,10 @@ let start () =
       exit 1
   end;
   if !batch_mode then (flush_all(); Profile.print_profile (); exit 0);
-  Lib.declare_initial_state ();
+  Lib.declare_initial_state ()
+
+let start () =
+  init ();
   Toplevel.loop();
   (* Initialise and launch the Ocaml toplevel *)
   Coqinit.init_ocaml_path();
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index ff4e169d9..42618505f 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -14,3 +14,10 @@
    produce the output state if any, and finally will launch [Toplevel.loop]. *)
 
 val start : unit -> unit
+
+(* [init] is already called by [start], but exported here to be reused 
+   by the Coq IDE. It does everything [start] does, except launching
+   the toplevel loop. *)
+
+val init : unit -> unit
+