coqide: preliminary support for mnemonics. Edit menu. Context help now works properly.

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

3 files changed, 129 insertions, 99 deletions

diff --git a/.depend b/.depend
index b016111d91..a4390d7ed2 100644
--- a/.depend
+++ b/.depend
@@ -40,10 +40,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 
@@ -63,9 +63,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 \
@@ -94,6 +91,9 @@ library/library.cmi: library/libnames.cmi library/libobject.cmi \
 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 
+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 
@@ -307,11 +307,11 @@ 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 
 translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \
     parsing/extend.cmi library/libnames.cmi kernel/names.cmi parsing/pcoq.cmi \
     lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi \
@@ -328,11 +328,11 @@ 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 
@@ -447,6 +447,12 @@ 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 \
+    ide/ideutils.cmo proofs/pfedit.cmi lib/pp_control.cmi ide/preferences.cmo \
+    lib/util.cmi toplevel/vernacexpr.cmo 
+ide/coqide.cmx: ide/coq.cmx ide/find_phrase.cmx ide/highlight.cmx \
+    ide/ideutils.cmx proofs/pfedit.cmx lib/pp_control.cmx ide/preferences.cmx \
+    lib/util.cmx toplevel/vernacexpr.cmx 
 ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
     kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
     tactics/hipattern.cmi ide/ideutils.cmo library/lib.cmi kernel/names.cmi \
@@ -463,12 +469,6 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
     proofs/refiner.cmx library/states.cmx proofs/tacmach.cmx kernel/term.cmx \
     lib/util.cmx toplevel/vernac.cmx toplevel/vernacentries.cmx \
     toplevel/vernacexpr.cmx ide/coq.cmi 
-ide/coqide.cmo: ide/coq.cmi ide/find_phrase.cmo ide/highlight.cmo \
-    ide/ideutils.cmo proofs/pfedit.cmi lib/pp_control.cmi ide/preferences.cmo \
-    lib/util.cmi toplevel/vernacexpr.cmo 
-ide/coqide.cmx: ide/coq.cmx ide/find_phrase.cmx ide/highlight.cmx \
-    ide/ideutils.cmx proofs/pfedit.cmx lib/pp_control.cmx ide/preferences.cmx \
-    lib/util.cmx toplevel/vernacexpr.cmx 
 ide/find_phrase.cmo: ide/ideutils.cmo 
 ide/find_phrase.cmx: ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmo 
@@ -599,6 +599,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 \
@@ -607,12 +613,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 \
@@ -695,34 +695,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 \
@@ -827,6 +817,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 
@@ -1835,10 +1835,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 \
@@ -2041,16 +2041,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 parsing/lexer.cmi library/lib.cmi \
-    library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
-    proofs/pfedit.cmi lib/pp.cmi translate/ppvernacnew.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 parsing/lexer.cmx library/lib.cmx \
-    library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
-    proofs/pfedit.cmx lib/pp.cmx translate/ppvernacnew.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 \
@@ -2111,6 +2101,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 parsing/lexer.cmi library/lib.cmi \
+    library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
+    proofs/pfedit.cmi lib/pp.cmi translate/ppvernacnew.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 parsing/lexer.cmx library/lib.cmx \
+    library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
+    proofs/pfedit.cmx lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx \
+    lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \
+    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \
     interp/constrextern.cmi interp/constrintern.cmi parsing/coqast.cmi \
     lib/dyn.cmi parsing/esyntax.cmi pretyping/evd.cmi interp/genarg.cmi \
@@ -2173,6 +2173,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 \
@@ -2189,18 +2201,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 \
@@ -2741,6 +2741,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 \
@@ -2765,14 +2773,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 \
@@ -3005,12 +3005,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 \
@@ -3065,8 +3065,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 \
@@ -3093,6 +3091,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/ide/coqide.ml b/ide/coqide.ml
index 3640f4b5be..136f4dc915 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -5,7 +5,8 @@ open Ideutils
 
 let out_some s = match s with | None -> assert false | Some f -> f
 
-let cb = GtkBase.Clipboard.get Gdk.Atom.clipboard
+let cb_ = ref None
+let cb () = out_some !cb_
 let last_cb_content = ref ""
 
 let yes_icon = "gtk-yes"
@@ -79,6 +80,8 @@ let get_current_tab_label () = get_tab_label (notebook())#current_page
 
 let reset_tab_label i = set_tab_label i (get_tab_label i)
 
+let to_do_on_page_switch = ref []
+  
 module Vector = struct 
   type 'a t = 'a array ref
   let create () = ref [||]
@@ -835,11 +838,7 @@ object(self)
 			   ~stop:input_buffer#end_iter
 			   "error";
 			   Highlight.highlight_current_line input_buffer));
-(*    ignore (input_buffer#add_selection_clipboard cb);*)
-(*    ignore (input_view#connect#paste_clipboard
-              (fun () ->  match GtkBase.Clipboard.wait_for_text cb with
-		 | None -> prerr_endline "None selected";
-		 | Some t -> prerr_endline "Some selected"))*)
+    ignore (input_buffer#add_selection_clipboard (cb()))
 end
 
 let create_input_tab filename =
@@ -903,13 +902,13 @@ let main () =
   let accel_group = factory#accel_group in
 
   (* File Menu *)
-  let file_menu = factory#add_submenu "File" in
+  let file_menu = factory#add_submenu "_File" in
   let file_factory = new GMenu.factory file_menu ~accel_group in
 
   (* File/Load Menu *)
-  let load_m = file_factory#add_item "Open/Create" ~key:GdkKeysyms._O in
+  let load_m = file_factory#add_item "_Open/Create" ~key:GdkKeysyms._O in
   let load_f () = 	  
-    match GToolbox.select_file ~title:"Load file" () with 
+    match GToolbox.select_file ~title:"_Load file" () with 
       | None -> ()
       | Some f -> 
 	  try
@@ -937,7 +936,7 @@ let main () =
   ignore (load_m#connect#activate load_f);
 
   (* File/Save Menu *)
-  let save_m = file_factory#add_item "Save" ~key:GdkKeysyms._S in
+  let save_m = file_factory#add_item "_Save" ~key:GdkKeysyms._S in
   let save_f () = 
     let current = get_current_view () in
     try (match current.filename with 
@@ -960,7 +959,7 @@ let main () =
   ignore (save_m#connect#activate save_f);
 
   (* File/Save As Menu *)
-  let saveas_m = file_factory#add_item "Save as" in
+  let saveas_m = file_factory#add_item "S_ave as" in
   let saveas_f () = 
     let current = get_current_view () in
     try (match current.filename with 
@@ -994,7 +993,7 @@ let main () =
   
   
   (* File/Save All Menu *)
-  let saveall_m = file_factory#add_item "Save All" in
+  let saveall_m = file_factory#add_item "Sa_ve All" in
   let saveall_f () = 
     Vector.iter 
       (fun {view = view ; filename = filename} -> 
@@ -1013,7 +1012,7 @@ let main () =
   ignore (saveall_m#connect#activate saveall_f);
 
   (* File/Revert Menu *)
-  let revert_m = file_factory#add_item "Revert" in
+  let revert_m = file_factory#add_item "_Revert" in
   revert_m#misc#set_state `INSENSITIVE;
 
   (* File/Print Menu *)
@@ -1032,7 +1031,7 @@ let main () =
 	  let c = Sys.command cmd in
 	  !flash_info (cmd ^ if c = 0 then " succeeded" else " failed")
   in
-  let print_m = file_factory#add_item "Print" ~callback:print_f in
+  let print_m = file_factory#add_item "_Print" ~callback:print_f in
 
   (* File/Export to Menu *)
   let export_f kind () =
@@ -1057,24 +1056,24 @@ let main () =
 	  let c = Sys.command cmd in
 	  !flash_info (cmd ^ if c = 0 then " succeeded" else " failed")
   in
-  let file_export_m =  file_factory#add_submenu "Export to" in
+  let file_export_m =  file_factory#add_submenu "E_xport to" in
 
   let file_export_factory = new GMenu.factory file_export_m ~accel_group in
   let export_html_m = 
-    file_export_factory#add_item "Html" ~callback:(export_f "html") 
+    file_export_factory#add_item "_Html" ~callback:(export_f "html") 
   in
   let export_latex_m = 
-    file_export_factory#add_item "LaTeX" ~callback:(export_f "latex")
+    file_export_factory#add_item "_LaTeX" ~callback:(export_f "latex")
   in
   let export_dvi_m = 
-    file_export_factory#add_item "Dvi" ~callback:(export_f "dvi") 
+    file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi") 
   in
   let export_ps_m = 
-    file_export_factory#add_item "Ps" ~callback:(export_f "ps") 
+    file_export_factory#add_item "_Ps" ~callback:(export_f "ps") 
   in
 
   (* File/Rehighlight Menu *)
-  let rehighlight_m = file_factory#add_item "Rehighlight" ~key:GdkKeysyms._L in
+  let rehighlight_m = file_factory#add_item "Reh_ighlight" ~key:GdkKeysyms._L in
   ignore (rehighlight_m#connect#activate 
 	    (fun () -> Highlight.highlight_all 
 	       (get_current_view()).view#buffer));
@@ -1102,10 +1101,36 @@ let main () =
 	| _ -> ()
     else exit 0
   in
-  let quit_m = file_factory#add_item "Quit" ~key:GdkKeysyms._Q ~callback:quit_f
+  let quit_m = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q ~callback:quit_f
   in
   ignore (w#event#connect#delete (fun _ -> quit_f (); true));
 
+  (* Edit Menu *)
+  let edit_menu = factory#add_submenu "_Edit" in
+  let edit_f = new GMenu.factory edit_menu ~accel_group in
+  ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
+	    (fun () -> GtkSignal.emit_unit
+	       (get_current_view()).view#as_view 
+	       GtkText.View.Signals.copy_clipboard));
+  ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
+	      (fun () -> GtkSignal.emit_unit
+		 (get_current_view()).view#as_view 
+		 GtkText.View.Signals.cut_clipboard));
+  ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
+    (fun () -> GtkSignal.emit_unit
+       (get_current_view()).view#as_view GtkText.View.Signals.paste_clipboard));
+  ignore (edit_f#add_separator ());
+  let read_only_i = edit_f#add_check_item "Read only" ~active:false
+		      ~callback:(fun b -> 
+				   (get_current_view()).view#set_editable 
+				   (not b)) 
+  in
+  to_do_on_page_switch := 
+  (fun i -> 
+     let v = (get_input_view i).view in
+     read_only_i#set_active (not v#editable)
+  )::!to_do_on_page_switch;
+  
   (* Navigation Menu *)
   let navigation_menu =  factory#add_submenu "Navigation" in
   let navigation_factory = new GMenu.factory navigation_menu ~accel_group ~accel_modi:[`CONTROL ; `MOD1] in
@@ -1307,14 +1332,14 @@ let main () =
     help_factory#add_item "Help for keyword" ~key:GdkKeysyms._F1
     ~callback:(fun () ->
 		 let av = out_some ((get_current_view ()).analyzed_view) in 
-		 match GtkBase.Clipboard.wait_for_text cb with
-		   | _ -> 
+		 match GtkBase.Clipboard.wait_for_text (cb ()) with
+		   | None -> 
 		       prerr_endline "None selected";
 		       av#help_for_keyword ()
-		   (* | Some t ->
+		   | Some t ->
  		       prerr_endline "Some selected";
 		       prerr_endline t;
-		       browse_keyword t*))
+		       browse_keyword t)
   in
   let _ = help_factory#add_separator () in
   let about_m = help_factory#add_item "About" in
@@ -1443,8 +1468,12 @@ let main () =
 		   hb#set_position (w/2);
 		   hb2#set_position (h*4/5)
 		 end
-	    ))
-    
+	    ));
+  ignore(nb#connect#switch_page 
+	   ~callback:
+	   (fun i -> List.iter (function f -> f i) !to_do_on_page_switch)
+	)
+
 let start () = 
   cant_break ();
   Coq.init ();
@@ -1453,6 +1482,7 @@ let start () =
      GtkMain.Rc.add_default_file (Filename.concat (Sys.getenv "HOME") ".coqiderc");
   with Not_found -> ());
   ignore (GtkMain.Main.init ());
+  cb_ := Some (GtkBase.Clipboard.get Gdk.Atom.primary);
   Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
 						      `WARNING;`CRITICAL]
     (fun ~level msg ->
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 52f7b3d28a..f0a0b4181c 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -22,7 +22,7 @@ let process_pending () =
     ignore (Glib.Main.iteration false) 
   done
 
-let debug = ref false
+let debug = ref true
 
 let prerr_endline s =
   if !debug then  prerr_endline s else ()
@@ -49,7 +49,7 @@ let try_export file_name s =
   with e -> prerr_endline (Printexc.to_string e)
 
 let browse url =
-  let l,r = Preferences.current.cmd_browse in
+  let l,r = current.cmd_browse in
   ignore (Sys.command (l ^ url ^ r))
 
 let url_for_keyword =