CoqIDE: robustesse / multi-buffers / menus / ... (utilisable)

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

10 files changed, 892 insertions, 433 deletions

diff --git a/.depend b/.depend
index c3a3695dc..04122e3b1 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 \
@@ -95,6 +92,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 
@@ -308,11 +308,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 \
@@ -329,11 +329,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 
@@ -443,6 +443,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 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 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 library/lib.cmi kernel/names.cmi lib/options.cmi \
@@ -459,10 +465,10 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.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 \
-    proofs/pfedit.cmi lib/pp_control.cmi lib/util.cmi toplevel/vernacexpr.cmo 
-ide/coqide.cmx: ide/coq.cmx ide/find_phrase.cmx ide/highlight.cmx \
-    proofs/pfedit.cmx lib/pp_control.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 
+ide/highlight.cmx: ide/ideutils.cmx 
 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 \
@@ -587,6 +593,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 \
@@ -595,12 +607,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 \
@@ -683,34 +689,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 \
@@ -815,6 +811,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 
@@ -1823,10 +1829,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 \
@@ -2029,16 +2035,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 \
@@ -2099,6 +2095,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 \
@@ -2161,6 +2167,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 \
@@ -2177,18 +2195,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 \
@@ -2729,6 +2735,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 \
@@ -2753,14 +2767,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 \
@@ -2933,12 +2939,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 \
@@ -2993,8 +2999,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 \
@@ -3021,6 +3025,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 b0aaedbc8..d7aa4c25f 100644
--- a/Makefile
+++ b/Makefile
@@ -420,7 +420,7 @@ beforedepend:: scripts/tolink.ml
 
 COQIDEBYTE=bin/coqide.byte$(EXE)
 COQIDEOPT=bin/coqide.opt$(EXE)
-COQIDECMO=ide/find_phrase.cmo ide/highlight.cmo ide/coq.cmo ide/coqide.cmo
+COQIDECMO=ide/ideutils.cmo 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
diff --git a/ide/.coqiderc b/ide/.coqiderc
new file mode 100644
index 000000000..f533310e7
--- /dev/null
+++ b/ide/.coqiderc
@@ -0,0 +1,18 @@
+style "views" {
+font_name = "Monospace 10"
+}
+class "GtkTextView" style "views"
+
+widget "*.*.*.*.*.ScriptWindow" style "views"
+widget "*.*.*.*.GoalWindow" style "views"
+widget "*.*.*.*.MessageWindow" style "views"
+
+style "menu" {
+font_name = "Serif 10"
+}
+
+
+class "GtkLabel" style "menu"
+
+gtk-key-theme-name = "Emacs"
+
diff --git a/ide/FAQ b/ide/FAQ
new file mode 100644
index 000000000..2d7d39bf5
--- /dev/null
+++ b/ide/FAQ
@@ -0,0 +1,19 @@
+Q1) How to enable Emacs keybindings?
+R1: Insert 
+	gtk-key-theme-name = "Emacs"
+    in your ".coqiderc" file. It may be in the current dir
+    or in $HOME dir.
+
+Q2) How to change the default font ?
+R2) Insert 
+	style "default" {
+	font_name = "Monospace 14"
+	}
+	class "GtkTextView" style "default"
+    in your .coqiderc file. See Q1.
+    You may replace Monospace 14 by anything reasonable describing 
+    a font. For example "Sans bold 22". See Pango Font Descriptions for more
+    informations (http://www.pango.org/).
+
+Q3) How to enable antialiased fonts?
+R3) Set the GDK_USE_XFT variable to 1.
diff --git a/ide/coq.gif b/ide/coq.gif
new file mode 100644
index 000000000..b4d5d20cc
--- /dev/null
+++ b/ide/coq.gif
diff --git a/ide/coq.ml b/ide/coq.ml
index 6c58d76e1..73345e06f 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -82,7 +82,9 @@ let print_toplevel_error exc =
     | 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),
+	(try Cerrors.explain_exn exc with e -> 
+	   str "Failed to explain error. This is an internal Coq error. Please report.\n"
+	   ++ str (Printexc.to_string  e)),
 	(if is_pervasive_exn exc then None else loc)
 
 let process_exn e = let s,loc=print_toplevel_error e in (msgnl s,loc)
@@ -188,8 +190,7 @@ let compute_reset_info = function
   | VernacDefinition (_, id, ProveBody _, _, _)
   | VernacStartTheoremProof (_, id, _, _, _) ->
       Reset (id, ref false)
-  | _ -> 
-      NoReset
+  | _ -> NoReset
 
 let reset_initial () = 
   prerr_endline "Reset initial called"; flush stderr;
diff --git a/ide/coqide.ml b/ide/coqide.ml
index fb36be297..d135ec6eb 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1,60 +1,160 @@
 open Vernacexpr
 open Coq
+open Ideutils
+
+  
+let out_some s = match s with | None -> assert false | Some f -> f
+
+let yes_icon = "gtk-yes"
+let no_icon = "gtk-no"
+let save_icon = "gtk-save"
+let saveas_icon = "gtk-save-as"
 
 let window_width = 1280
 let window_height = 1024
 
-let byte_offset_to_char_offset s byte_offset = 
-  assert (byte_offset < String.length s);
-  let count_delta = ref 0 in
-  for i = 0 to byte_offset do
-    let code = Char.code s.[i] in
-    if code >= 0x80 && code < 0xc0 then incr count_delta
-  done;
-  byte_offset - !count_delta
-
-let initial_font_name =  "Monospace 14"
-let monospace_font = ref (Pango.Font.from_string initial_font_name)
-let general_font = ref !monospace_font
-let lower_view_general_font = ref !general_font
-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 (font_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 initial_cwd = Sys.getcwd ()
+
+let default_general_font_name = "Sans 14"
+let default_monospace_font_name = "Monospace 14"
+
+let manual_monospace_font = ref None
+let manual_general_font = ref None
+
+let has_config_file = (Sys.file_exists ".coqiderc") || 
+		      (try Sys.file_exists (Filename.concat (Sys.getenv "HOME") ".coqiderc")
+		       with Not_found -> false)
+
+let _ = if not has_config_file then 
+  manual_monospace_font := Some (Pango.Font.from_string default_monospace_font_name);
+  manual_general_font := Some (Pango.Font.from_string default_general_font_name)
+
+
+let (font_selector:GWindow.font_selection_dialog option ref) = ref None
+let (message_view:GText.view option ref) = ref None
+let (proof_view:GText.view option ref) = ref None
+
+let (_notebook:GPack.notebook option ref) = ref None
+let notebook () = out_some !_notebook
+
+let decompose_tab w = 
+  let vbox = new GPack.box ((Gobject.try_cast w "GtkBox"):Gtk.box Gtk.obj) in
+  let l = vbox#children in
+  match l with 
+    | [img;lbl] -> 
+	let img = new GMisc.image 
+		    ((Gobject.try_cast img#as_widget "GtkImage"):
+		       Gtk.image Gtk.obj) 
+	in
+	let lbl = GMisc.label_cast lbl in
+	vbox,img,lbl
+    | _ -> assert false
+	
+let set_tab_label i n =
+  let nb = notebook () in
+  let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget in
+  lbl#set_markup n
+
+let set_tab_image i s = 
+  let nb = notebook () in
+  let _,img,_ = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget in
+  img#set_stock s ~size:1
+
+let set_current_tab_image s = set_tab_image (notebook())#current_page s
+  
+let set_current_tab_label n = 
+  set_tab_label (notebook())#current_page n 
+
+let get_tab_label i =
+  let nb = notebook () in
+  let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget in
+  lbl#text
+
+let get_current_tab_label () = get_tab_label (notebook())#current_page
+
+let reset_tab_label i = set_tab_label i (get_tab_label i)
+
+module Vector = struct 
+  type 'a t = 'a array ref
+  let create () = ref [||]
+  let get t = Array.get !t
+  let set t = Array.set !t
+  let append t e = t := Array.append !t [|e|]; (Array.length !t)-1
+  let iter f t =  Array.iter f !t
+  let exists f t =
+    let l = Array.length !t in
+    let rec test i = i < l && (f !t.(i) || test (i+1)) in 
+    test 0
+end
+
+type viewable_script =
+    {view : GText.view;
+     mutable deactivate : unit -> unit;
+     mutable activate : unit -> unit;
+     mutable filename : string option
+    }
+
+let (input_views:viewable_script Vector.t) = Vector.create ()
+
+let crash_save i =
+  Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files";
+  let count = ref 0 in 
+  Vector.iter 
+    (function {view=view;filename=filename} -> 
+       let filename = match filename with 
+	 | None -> incr count; "Unamed_coqscript_"^(string_of_int !count)^".crashcoqide"
+	 | Some f -> f^".crashcoqide"
+       in
+       try 
+	 try_export filename (view#buffer#get_text ());
+	 Pervasives.prerr_endline ("Saved "^filename)
+       with _ -> Pervasives.prerr_endline ("Could not save "^filename)
+    )
+    input_views;
+  Pervasives.prerr_endline "Done. Please report.";
+  exit i
+
+let _ = 
+  let signals_to_catch = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup; Sys.sigill; 
+			  Sys.sigint; Sys.sigpipe; Sys.sigquit; Sys.sigsegv; 
+			  Sys.sigterm; Sys.sigusr2] 
+  in List.iter (fun i -> Sys.set_signal i (Sys.Signal_handle crash_save)) signals_to_catch
+
+let add_input_view tv = 
+  Vector.append input_views tv
+
+let get_input_view i = Vector.get input_views i
+
+let active_view = ref None
+
+let get_active_view () = Vector.get input_views (out_some !active_view)
+
+let set_active_view i = 
+  (match !active_view with  None -> () | Some i -> 
+     reset_tab_label i);
+  (notebook ())#goto_page i; 
+  let txt = get_current_tab_label () in
+  set_current_tab_label ("<span background=\"light green\">"^txt^"</span>");
+  active_view := Some i
+
+(* let kill_input_view i = 
+  if (Array.length !input_views) <= 1 then input_views := [||]
+  else
+    let r = Array.create (Array.length !input_views) !input_views.(0) in
+    Array.iteri (fun j tv -> 
+		   if j < i then r.(j) <- !input_views.(j) 
+		   else if j > i then r.(j-1) <- !input_views.(j))
+      !input_views;
+    input_views := r
+*)
+
+let get_current_view () = Vector.get input_views (notebook ())#current_page
 
 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
@@ -65,8 +165,6 @@ 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:Util.loc * Vernacexpr.vernac_expr;
@@ -135,14 +233,11 @@ let set_break () =
 let unset_break () = 
   Sys.set_signal Sys.sigusr1 Sys.Signal_ignore
 
+(* Signal sigusr1 is used to stop coq computation *)
 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 =
@@ -154,28 +249,21 @@ let read_stdout,clear_stdout =
   (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
+    (if not (it#begins_tag (Some tag)) 
+     then it#backward_to_tag_toggle (Some tag)
+     else it#copy),
+    (if not (it#ends_tag (Some tag))
+     then it#forward_to_tag_toggle (Some tag)
+     else it#copy)
+
+let rec analyze_all index =
+  let {view = input_view } as current_all = get_input_view index in
+  let (proof_view:GText.view) = out_some !proof_view in
+  let (message_view:GText.view) = out_some !message_view in
+  let input_buffer = input_view#buffer in
+  let proof_buffer = proof_view#buffer in
+  let message_buffer = message_view#buffer in
   let insert_message s =
     message_buffer#insert s;
     message_view#misc#draw None
@@ -184,57 +272,45 @@ let analyze_all
     message_buffer#set_text s;
     message_view#misc#draw None
   in
-  let clear_message () =
-    message_buffer#set_text ""
+  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))));
+  ignore (message_buffer#connect#after#insert_text
+	    ~callback:(fun it s -> ignore 
+			 (message_view#scroll_to_mark
+			    ~within_margin:0.49
+			    `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") 
+      (`NAME "start_of_input") 
   in
+  ignore (input_buffer#connect#modified_changed
+	 ~callback:(fun () ->
+		      if input_buffer#modified then 
+			set_tab_image index 
+			  (match current_all.filename with 
+			     | None -> saveas_icon
+			     | Some _ -> save_icon
+			  )
+		      else set_tab_image index yes_icon;
+		   ));
   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 = input_buffer#get_slice ~start ~stop () in
-    let convert_pos = byte_offset_to_char_offset s in
-    let lb = Lexing.from_string s in
-    try 
-      while true do
-	process_pending ();
-	let b,e,o=Highlight.next_order lb in
-	let b,e = convert_pos b,convert_pos e 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 ())
+			 ~stop:input_buffer#end_iter
+			 "error";
+			 Highlight.highlight_current_line input_buffer));
+  let get_insert () = get_insert input_buffer in
+  let recenter_insert () = ignore (input_view#scroll_to_iter 
+				     ~within_margin:0.10 
+				     (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 "";
+    proof_view#buffer#set_text "";
     let s = Coq.get_curent_goals () in
-    let last_shown_area = proof_buffer#create_tag
-			    ~properties:[`BACKGROUND "light blue"]
-			    ()
+    let last_shown_area = proof_buffer#create_tag [`BACKGROUND "light blue"]
     in
     match s with 
       | [] -> proof_buffer#insert (Coq.print_no_goal ())
@@ -244,7 +320,7 @@ let analyze_all
 				 goal_nb
 				 (if goal_nb<=1 then "" else "s"));
 	  let coq_menu commands = 
-	    let tag = proof_buffer#create_tag ()
+	    let tag = proof_buffer#create_tag []
 	    in 
 	    ignore
 	      (tag#connect#event ~callback:
@@ -276,8 +352,8 @@ let analyze_all
 			  end
 		      | `MOTION_NOTIFY -> 
 			  proof_buffer#remove_tag
-			  ~start:proof_buffer#get_start_iter
-			  ~stop:proof_buffer#get_end_iter
+			  ~start:proof_buffer#start_iter
+			  ~stop:proof_buffer#end_iter
 			  last_shown_area;
 			  let s,e = find_tag_limits tag 
 				      (new GText.iter it) 
@@ -296,7 +372,7 @@ let analyze_all
 	       let tag = coq_menu (hyp_menu hyp) in
 	       proof_buffer#insert ~tags:[tag] (s^"\n"))
 	    hyps;
-	  proof_buffer#insert ("--------------------------------------(1/"^
+	  proof_buffer#insert ("---------------------------------------(1/"^
 			       (string_of_int goal_nb)^
 			       ")\n") 
 	  ;
@@ -304,16 +380,15 @@ let analyze_all
 	  let _,_,_,sconcl = concl in
 	  proof_buffer#insert ~tags:[tag] sconcl;
 	  proof_buffer#insert "\n";
-	  let my_mark = proof_buffer#get_mark ~name:"end_of_conclusion" in
+	  let my_mark = `NAME "end_of_conclusion" in
 	  proof_buffer#move_mark
-	    ~where:((proof_buffer#get_iter_at_mark proof_buffer#get_insert))
-	    my_mark;
+	    ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
 	  proof_buffer#insert "\n\n";
 	  let i = ref 1 in
 	  List.iter 
 	    (function (_,(_,_,_,concl)) -> 
 	       incr i;
-	       proof_buffer#insert ("----------------------------------------("^
+	       proof_buffer#insert ("--------------------------------------("^
 				    (string_of_int !i)^
 				    "/"^
 				    (string_of_int goal_nb)^
@@ -322,8 +397,8 @@ let analyze_all
 	       proof_buffer#insert "\n\n";
 	    )
 	    r;
-	  ignore (proof_view#scroll_to_mark my_mark)
-  and send_to_coq phrase show_output show_error localize = 
+	  ignore (proof_view#scroll_to_mark my_mark) 
+  and send_to_coq phrase show_output show_error localize =
     try
       !push_info "Coq is computing";
       (out_some !status)#misc#draw None;
@@ -353,32 +428,48 @@ let analyze_all
 		  let start = convert_pos start in
 		  let stop = convert_pos stop in
 		  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);
+		  let starti = i#forward_chars start in
+		  let stopi = i#forward_chars stop in
 		  input_buffer#apply_tag_by_name "error"
    		    ~start:starti
 		    ~stop:stopi
 	   ));
       None
   and find_phrase_starting_at (start:GText.iter) = 
+    let trash_bytes = ref "" in
     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;
+      let i = ref 0 in
+      let n_trash = String.length !trash_bytes in
+      String.blit !trash_bytes 0 s 0 n_trash;
+      i := n_trash;
+      try
+	while !i <= count - 1 do
+	  let c = end_iter#char in
+	  if c = 0 then raise (Stop !i);
+	  let c' = Glib.Utf8.from_unichar c in
+	  let n = String.length c' in
+	  if n > count - !i  then 
+	    begin
+	      let ri = count - !i in
+	      String.blit c' 0 s !i ri;
+	      trash_bytes := String.sub c' ri (n-ri);
+	      i := count ;
+	    end else begin
+	      String.blit c' 0 s !i n;
+	      i:= !i + n
+	    end;
+	  if not end_iter#nocopy#forward_char then 
+	    raise (Stop !i)
+	done;
 	count
       with Stop x -> x
     in
     try
       Find_phrase.length := 0;
+      trash_bytes := "";
       let phrase = Find_phrase.next_phrase (Lexing.from_function lexbuf_function) in
-      end_iter#set_offset (start#get_offset + !Find_phrase.length);
+      end_iter#nocopy#set_offset (start#offset + !Find_phrase.length);
       Some (start,end_iter)
     with _ -> None
   and process_next_phrase display_goals = 
@@ -387,21 +478,23 @@ let analyze_all
     with None -> false
       | Some(start,stop) ->
 	  let b = input_buffer in
-	  let phrase = b#get_slice ~start ~stop () in
+	  let phrase = start#get_slice ~stop in
 	  match send_to_coq phrase true true true with
 	    | Some ast ->
 		begin
-		  b#move_mark_by_name ~where:stop "start_of_input";
+		  b#move_mark ~where:stop (`NAME "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
+		    begin
+		      b#place_cursor stop;
+		      recenter_insert () 
+		    end;
+		  let start_of_phrase_mark = `MARK (b#create_mark start) in
+		  let end_of_phrase_mark = `MARK (b#create_mark stop) in
 		  push_phrase start_of_phrase_mark end_of_phrase_mark ast;
 		  if display_goals then
-		    (try show_goals () with e -> ());
+		    (try show_goals () with e -> 
+		       prerr_endline (Printexc.to_string e);());
 		  true;
 		end
 	    | None -> false
@@ -415,12 +508,12 @@ let analyze_all
 	      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#move_mark ~where:stop (`NAME "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
+	    let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in
+	    let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
 	    push_phrase start_of_phrase_mark end_of_phrase_mark ast;
 	    (try show_goals () with e -> ());
 	    true
@@ -449,7 +542,7 @@ let analyze_all
       (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#move_mark ~where:start (`NAME "start_of_input");
 	 input_buffer#remove_tag_by_name "processed" ~start ~stop;
 	 input_buffer#delete_mark inf.start;
 	 input_buffer#delete_mark inf.stop;
@@ -495,23 +588,21 @@ let analyze_all
 	(match undos with 
 	   | None -> synchro () 
 	   | Some n -> try Pfedit.undo n with _ -> synchro ());
-	let start = if is_empty () then input_buffer#get_start_iter 
+	let start = if is_empty () then input_buffer#start_iter 
 	else input_buffer#get_iter_at_mark (top ()).stop 
 	in
 	input_buffer#remove_tag_by_name 
 	  ~start 
 	  ~stop:(get_start_of_input ()) 
 	  "processed";
-	input_buffer#move_mark_by_name ~where:start "start_of_input";
+	input_buffer#move_mark ~where:start (`NAME "start_of_input");
 	input_buffer#place_cursor start;
 	(try show_goals () with e -> ());
 	clear_stdout ();
 	clear_message ()
       end
   in
-  let backtrack_to_insert () = 
-    backtrack_to (get_insert ())
-  in
+  let backtrack_to_insert () = backtrack_to (get_insert ()) in
   let undo_last_step () = 
     try
       let last_command = top () in
@@ -521,10 +612,11 @@ let analyze_all
 	  ~start
 	  ~stop:(input_buffer#get_iter_at_mark last_command.stop) 
 	  "processed";
-	input_buffer#move_mark_by_name 
+	input_buffer#move_mark
 	  ~where:start
-	  "start_of_input";
+	  (`NAME "start_of_input");
 	input_buffer#place_cursor start;
+	recenter_insert ();
 	(try show_goals () with e -> ());
 	clear_message ()
       in
@@ -548,37 +640,6 @@ let analyze_all
       end
     with
       | Size 0 -> !flash_info "Nothing to Undo"
-	  (*    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 ();
@@ -589,110 +650,114 @@ let analyze_all
 	      (fun (cp,ip) -> 
 		 insert_this_phrase_on_success true 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 backtrack_to_insert ()
-		     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)
+  let active_keypress_handler k = 
+    match GdkEvent.Key.state k with
+      | l when List.mem `MOD1 l ->
+	  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 backtrack_to_insert ()
+	  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())#backward_word_start in
+		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
+      | l when List.mem `CONTROL l -> 
+	  let k = GdkEvent.Key.keyval k in
+	  if GdkKeysyms._c=k
+	  then break ();
+	  false
+      | l -> false
+  in 
+  let disconnected_keypress_handler k = 
+    match GdkEvent.Key.state k with
+      | l when List.mem `MOD1 l ->
+	  let k = GdkEvent.Key.keyval k in
+	  if (GdkKeysyms._Down=k || GdkKeysyms._Right=k
+	      || GdkKeysyms._Left=k || GdkKeysyms._r=k
+              ||  GdkKeysyms._Up=k)
+	  then activate_input index;
+	  true
+      | l when List.mem `CONTROL l -> 
+	  let k = GdkEvent.Key.keyval k in
+	  if GdkKeysyms._c=k
+	  then break ();
+	  false
+      | l -> false
+  in 
+  let deact_id = ref None in
+  let act_id = ref None in
+  let deactivate_function,activate_function = 
+    (fun () -> 
+       (match !act_id with None -> () 
+	  | Some id ->
+	      reset_initial ();
+	      input_view#misc#disconnect id;
+	      prerr_endline "DISCONNECTED old active : ";
+	      print_id id;
+       );
+       deact_id := Some 
+	 (input_view#event#connect#key_press disconnected_keypress_handler);
+       prerr_endline "CONNECTED  inactive : ";
+       print_id (out_some !deact_id)
+    ),
+    (fun () -> 
+       (match !deact_id with None -> () 
+	  | Some id -> input_view#misc#disconnect id;
+	      prerr_endline "DISCONNECTED old inactive : ";
+	      print_id id
+       );
+       act_id := Some 
+	 (input_view#event#connect#key_press active_keypress_handler);
+       prerr_endline "CONNECTED active : ";
+       print_id (out_some !act_id);
+       Sys.chdir (match (Vector.get input_views index).filename with
+		       | None -> initial_cwd
+		       | Some f -> Filename.dirname f
+		 )
+    )
   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 r = Vector.get input_views index in
+  r.deactivate <- deactivate_function; r.activate <- activate_function;
   let electric_handler () = 
     input_buffer#connect#insert_text ~callback:
       (fun it x -> 
@@ -712,28 +777,314 @@ let analyze_all
 	 last_index := not !last_index;)
   in
   ()
+and activate_input i = 
+  (match !active_view with
+     | None -> () 
+     | Some n -> 
+	 prerr_endline ("DEACT"^(string_of_int n));
+	 let f = (Vector.get input_views n).deactivate in 
+	 f()
+  );
+  let activate_function = (Vector.get input_views i).activate in
+  prerr_endline ("ACT"^(string_of_int i));
+  activate_function ();
+  prerr_endline ("ACTIVATED"^(string_of_int i));
+  set_active_view i
 
+let create_input_tab filename =
+  let b = GText.buffer () in 
+  let tablabel = GMisc.label () in 
+  let v_box = GPack.hbox ~homogeneous:false () in
+  let image = GMisc.image ~packing:v_box#pack () in
+  let label = GMisc.label ~text:filename ~packing:v_box#pack () in
+  let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT
+	      ~packing:((notebook ())#append_page ~tab_label:v_box#coerce) () 
+  in 
+  let sw1 = GBin.scrolled_window
+	      ~vpolicy:`AUTOMATIC 
+	      ~hpolicy:`AUTOMATIC
+	      ~packing:fr1#add () 
+  in
+  let tv1 = GText.view ~buffer:b ~packing:(sw1#add) () in
+  tv1#misc#set_name "ScriptWindow";
+  let _ = tv1#set_editable true in
+  let _ = tv1#set_wrap_mode `CHAR in
+  b#place_cursor ~where:(b#start_iter);
+  ignore (tv1#event#connect#button_press ~callback:
+	    (fun ev -> GdkEvent.Button.button ev = 3));
+  tv1#misc#grab_focus ();
+  ignore (tv1#buffer#create_mark 
+	    ~name:"start_of_input" 
+	    tv1#buffer#start_iter);
+  ignore (tv1#buffer#create_tag 
+	    ~name:"to_process" 
+	    [`BACKGROUND "light blue" ;`EDITABLE false]);
+  ignore (tv1#buffer#create_tag 
+	    ~name:"processed" 
+	    [`BACKGROUND "light green" ;`EDITABLE false]);
+  ignore (tv1#buffer#create_tag 
+	    ~name:"error" 
+	    [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]);
+  ignore (tv1#buffer#create_tag 
+	    ~name:"kwd" 
+	    [`FOREGROUND "blue"]);
+  ignore (tv1#buffer#create_tag 
+	    ~name:"decl" 
+	    [`FOREGROUND "orange red"]);
+  ignore (tv1#buffer#create_tag 
+	    ~name:"comment" 
+	    [`FOREGROUND "brown"]);
+  ignore (tv1#buffer#create_tag 
+	    ~name:"reserved" 
+	    [`FOREGROUND "dark red"]);
+  tv1
+  
 let main () = 
   let w = GWindow.window 
-	    ~allow_grow:true ~allow_shrink:true ~width:window_width ~height:window_height ~title:"CoqIde" ()
+	    ~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
+
+  (* File Menu *)
   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
 
+  (* File/Load Menu *)
+  let load_m = file_factory#add_item "Open" ~key:GdkKeysyms._O in
+  let load_f () = 	  
+    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
+	    let view = create_input_tab (Filename.basename f) in
+	    (match !manual_monospace_font with
+	       | None -> ()
+	       | Some n -> view#misc#modify_font n);
+	    let index = add_input_view {view = view;
+					activate = (fun () -> ());
+					deactivate = (fun () -> ());
+					filename = Some f
+				       }
+	    in
+	    analyze_all index;
+	    activate_input index;
+	    let input_buffer = view#buffer in
+	    input_buffer#set_text s;
+	    input_buffer#place_cursor input_buffer#start_iter;
+	    Highlight.highlight_all input_buffer;
+	    input_buffer#set_modified false
+	  with e -> !flash_info "Load failed"
+  in
+  ignore (load_m#connect#activate load_f);
+
+  (* File/Save Menu *)
+  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 
+	   | None -> 
+	       begin match GToolbox.select_file ~title:"Save file" ()
+	       with
+		 | None -> ()
+		 | Some f -> 
+		     try_export f (current.view#buffer#get_text ());
+		     current.filename <- Some f;
+		     set_current_tab_label (Filename.basename f);
+		     current.view#buffer#set_modified false
+	       end
+	   | Some f -> 
+	       try_export f (current.view#buffer#get_text ());
+	       current.view#buffer#set_modified false);
+      !flash_info "Saved"
+    with e -> !flash_info "Save failed"
+  in   
+  ignore (save_m#connect#activate save_f);
+
+  (* File/Save As Menu *)
+  let saveas_m = file_factory#add_item "Save as" in
+  let saveas_f () = 
+    let current = get_current_view () in
+    try (match current.filename with 
+	   | None -> 
+	       begin match GToolbox.select_file ~title:"Save file as" ()
+	       with
+		 | None -> ()
+		 | Some f -> 
+		     try_export f (current.view#buffer#get_text ());
+		     current.filename <- Some f;
+		     set_current_tab_label (Filename.basename f);
+		     current.view#buffer#set_modified false
+	       end
+	   | Some f -> 
+	       begin match GToolbox.select_file 
+		 ~dir:(ref (Filename.dirname f)) 
+		 ~filename:(Filename.basename f)
+		 ~title:"Save file as" ()
+	       with
+		 | None -> ()
+		 | Some f -> 
+		     try_export f (current.view#buffer#get_text ());
+		     current.filename <- Some f;
+		     set_current_tab_label (Filename.basename f);
+		     current.view#buffer#set_modified false
+	       end);
+      !flash_info "Saved"
+    with e -> !flash_info "Save failed"
+  in   
+  ignore (saveas_m#connect#activate saveas_f);
+  
+  
+  (* File/Save All Menu *)
+  let saveall_m = file_factory#add_item "Save All" in
+  let saveall_f () = 
+    Vector.iter 
+      (fun {view = view ; filename = filename} -> 
+	 match filename with 
+	   | None -> ()
+	   | Some f ->
+	       try_export f (view#buffer#get_text ());
+	       view#buffer#set_modified false
+      )  input_views
+  in
+  let has_something_to_save () = 
+    Vector.exists
+      (fun {view=view} -> view#buffer#modified)
+      input_views
+  in
+  ignore (saveall_m#connect#activate saveall_f);
+
+  (* File/Revert Menu *)
+  let revert_m = file_factory#add_item "Revert" in
+  revert_m#misc#set_state `INSENSITIVE;
+
+  (* File/Print Menu *)
+  let print_m = file_factory#add_item "Print" in
+  print_m#misc#set_state `INSENSITIVE;
+
+  (* File/Export to Menu *)
+  let file_export_m =  file_factory#add_submenu "Export 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" in
+  export_html_m#misc#set_state `INSENSITIVE;
+  
+  let export_latex_m = file_export_factory#add_item "LaTeX" in
+  export_latex_m#misc#set_state `INSENSITIVE;
+
+  let export_dvi_m = file_export_factory#add_item "Dvi" in
+  export_dvi_m#misc#set_state `INSENSITIVE;
+
+  let export_ps_m = file_export_factory#add_item "Ps" in
+  export_ps_m#misc#set_state `INSENSITIVE;
+
+  (* File/Rehighlight Menu *)
+  let rehighlight_m = file_factory#add_item "Rehighlight" ~key:GdkKeysyms._L in
+  ignore (rehighlight_m#connect#activate 
+	    (fun () -> Highlight.highlight_all 
+	       (get_current_view()).view#buffer));
+
+  (* File/Refresh Menu *)
+  let refresh_m = file_factory#add_item "Restart all" ~key:GdkKeysyms._R in
+  refresh_m#misc#set_state `INSENSITIVE;
+
+  (* Fiel/Quit Menu *)
+  let quit_f () =
+    if has_something_to_save () then 
+      match (GToolbox.question_box ~title:"Quit"
+	       ~buttons:["Save Named Buffers and Quit";
+			 "Don't Save and Quit";
+			 "Don't Quit"] 
+	       ~default:0
+	       ~icon:
+	       (let img = GMisc.image () in
+		img#set_stock "gtk-dialog-warning" ~size:6;
+		img#coerce)
+	       "There are unsaved buffers"
+	    )
+      with 1 -> saveall_f () ; exit 0
+	| 2 -> exit 0
+	| _ -> ()
+    else exit 0
+  in
+  let quit_m = file_factory#add_item "Quit" ~key:GdkKeysyms._Q ~callback:quit_f
+  in
+  ignore (w#event#connect#delete (fun _ -> quit_f (); true));
+
+  (* Navigation Menu *)
+  let navigation_menu =  factory#add_submenu "Navigation" in
+  let navigation_factory = new GMenu.factory navigation_menu ~accel_group in
+  ignore (navigation_factory#add_item "Forward");
+  ignore (navigation_factory#add_item "Backward");
+  ignore (navigation_factory#add_item "Forward to");
+  ignore (navigation_factory#add_item "Backward to");
+  ignore (navigation_factory#add_item "Start");
+  ignore (navigation_factory#add_item "End");
+
+  (* Tactics Menu *)
+  let tactics_menu =  factory#add_submenu "Tactics" in
+  let tactics_factory = new GMenu.factory tactics_menu ~accel_group in
+  ignore (tactics_factory#add_item "Auto");
+  ignore (tactics_factory#add_item "Auto with *");
+  ignore (tactics_factory#add_item "EAuto");
+  ignore (tactics_factory#add_item "EAuto with *");
+  ignore (tactics_factory#add_item "Intuition");
+  ignore (tactics_factory#add_item "Omega");
+  ignore (tactics_factory#add_item "Simpl");
+  ignore (tactics_factory#add_item "Tauto");
+  ignore (tactics_factory#add_item "Trivial");
+  
+  (* Templates Menu *)
+  let templates_menu =  factory#add_submenu "Templates" in
+  let templates_factory = new GMenu.factory templates_menu ~accel_group ~accel_modi:[`MOD1] in
+  let templates_tactics = templates_factory#add_submenu "Tactics" in
+  let templates_tactics_factory = new GMenu.factory templates_tactics ~accel_group in
+  ignore (templates_tactics_factory#add_item "Auto");
+  ignore (templates_tactics_factory#add_item "Auto with *");
+  ignore (templates_tactics_factory#add_item "EAuto");
+  ignore (templates_tactics_factory#add_item "EAuto with *");
+  ignore (templates_tactics_factory#add_item "Intuition");
+  ignore (templates_tactics_factory#add_item "Omega");
+  ignore (templates_tactics_factory#add_item "Simpl");
+  ignore (templates_tactics_factory#add_item "Tauto");
+  ignore (templates_tactics_factory#add_item "Trivial");
+  let templates_commands = templates_factory#add_submenu "Commands" in
+  let templates_commands_factory = new GMenu.factory templates_commands 
+				     ~accel_group 
+				     ~accel_modi:[`MOD1]
+  in
+  (* Templates/Commands/Lemma *)
+  let callback () = 
+    let {view = view } = get_current_view () in
+    if (view#buffer#insert_interactive "Lemma new_lemma : .\nProof.\n\nSave.\n") then
+      begin
+	let iter = view#buffer#get_iter_at_mark `INSERT in
+	ignore (iter#nocopy#backward_chars 19);
+	view#buffer#move_mark `INSERT iter;
+	ignore (iter#nocopy#backward_chars 9);
+	view#buffer#move_mark `SEL_BOUND iter;
+	Highlight.highlight_all view#buffer
+      end
+  in
+  ignore (templates_commands_factory#add_item "Lemma _" ~callback ~key:GdkKeysyms._L);
+
+  
+  (* Commands Menu *)
+  let commands_menu =  factory#add_submenu "Commands" in
+  let commands_factory = new GMenu.factory commands_menu ~accel_group in
+  ignore (commands_factory#add_item "Compile");
+  ignore (commands_factory#add_item "Make");
+  ignore (commands_factory#add_item "Make Makefile");
+
+  (* Configuration Menu *)
   let configuration_menu = factory#add_submenu "Configuration" in
   let configuration_factory = new GMenu.factory configuration_menu ~accel_group
   in
@@ -741,12 +1092,12 @@ let main () =
     configuration_factory#add_item "Customize colors"
       ~callback:(fun () -> !flash_info "Not implemented")
   in
-  let font_selector = 
-    GWindow.font_selection_dialog 
-      ~title:"Select font..."
-      ~modal:true ()
-  in
-  font_selector#selection#set_font_name initial_font_name;
+  font_selector := 
+  Some (GWindow.font_selection_dialog 
+	  ~title:"Select font..."
+	  ~modal:true ());
+  let font_selector = out_some !font_selector in
+  font_selector#selection#set_font_name default_monospace_font_name;
   font_selector#selection#set_preview_text 
     "Lemma Truth: (p:Prover) `p < Coq`. Proof. Auto with *. Save."; 
   let customize_fonts_m = 
@@ -755,11 +1106,8 @@ let main () =
   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
+  _notebook := Some (GPack.notebook ~packing:hb#add1 ());
+  let nb = notebook () 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);
@@ -772,7 +1120,6 @@ let main () =
 	      ~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;
@@ -780,16 +1127,13 @@ let main () =
   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
+  tv2#misc#set_name "GoalWindow";
   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 tb2 = tv2#buffer in
   let tv3 = GText.view ~packing:(sw3#add) () in
+  tv2#misc#set_name "MessageWindow";
+  let _ = tv2#set_wrap_mode `CHAR 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
@@ -805,7 +1149,7 @@ let main () =
 					 ~y 
 			 in
 			 let it = tv2#get_iter_at_location ~x:b_x ~y:b_y in
-			 let tags = it#get_tags in
+			 let tags = it#tags in
 			 List.iter 
 			   ( fun t ->
 			       ignore (GtkText.Tag.event 
@@ -824,72 +1168,61 @@ let main () =
 			    | None -> ()
 			    | Some n -> 
 				let pango_font = Pango.Font.from_string n in
-				tv1#misc#modify_font pango_font;
 				tv2#misc#modify_font pango_font;
 				tv3#misc#modify_font pango_font;
+				Vector.iter 
+				  (fun {view=view} -> view#misc#modify_font pango_font)
+				  input_views;
+				manual_monospace_font := Some pango_font
 			 );
 			 font_selector#misc#hide ()));
 
   (try 
      let startup_image = GdkPixbuf.from_file "coq.gif" in
-     tv2#get_buffer#insert_pixbuf ~iter:tv2#get_buffer#get_start_iter 
+     tv2#buffer#insert_pixbuf ~iter:tv2#buffer#start_iter 
        ~pixbuf:startup_image;
-     tv2#get_buffer#insert ~iter:tv2#get_buffer#get_start_iter "\t\t";
+     tv2#buffer#insert ~iter:tv2#buffer#start_iter "\t\t";
    with _ -> ());
-  tv2#get_buffer#insert "\nCoqIde: an experimental Gtk2 interface for Coq.\n";
-  tv2#get_buffer#insert (try_convert (Coq.version ()));
-  b#place_cursor ~where:(b#get_start_iter);
-  (*  let _ =  refresh_m#connect#activate 
-      ~callback:(fun () -> analyze_all tv1 tv2 tv3) 
-      in
-  *)
+  tv2#buffer#insert "\nCoqIde: an experimental Gtk2 interface for Coq.\n";
+  tv2#buffer#insert (try_convert (Coq.version ()));
   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 
+  ignore (tv2#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 blue" ;`EDITABLE false] ());
-  ignore (tv1#get_buffer#create_tag 
-	    ~name:"processed" 
-	    ~properties:[`BACKGROUND "light 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 
+	    tv2#buffer#start_iter);
+  ignore (tv3#buffer#create_tag 
 	    ~name:"error" 
-	    ~properties:[`FOREGROUND "red"] ());
+	    [`FOREGROUND "red"]);
   w#show ();
-  analyze_all tv1 tv2 tv3
+  message_view := Some tv3;
+  proof_view := Some tv2;
+  let view = create_input_tab "New File" in
+  let index = add_input_view {view = view;
+			      activate = (fun () -> ());
+			      deactivate = (fun () -> ());
+			      filename = None}
+  in
+  analyze_all index;
+  activate_input index;
+  set_tab_image index yes_icon;
 
+  (match !manual_monospace_font with 
+     | None -> ()
+     | Some f -> view#misc#modify_font f; tv2#misc#modify_font f; tv3#misc#modify_font f)
+    
 let start () = 
   cant_break ();
   Coq.init ();
+  GtkMain.Rc.add_default_file ".coqiderc";
+  (try 
+     GtkMain.Rc.add_default_file (Filename.concat (Sys.getenv "HOME") ".coqiderc");
+  with Not_found -> ());
   ignore (GtkMain.Main.init ());
   Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
 						      `WARNING;`CRITICAL]
@@ -898,7 +1231,12 @@ let start () =
     );
   main ();
   Sys.catch_break true;
+  while true do 
     try 
       GMain.Main.main ()
     with 
-    Sys.Break -> prerr_endline "Interrupted." ; ()
+      | Sys.Break -> prerr_endline "Interrupted." ; flush stderr
+      | e -> 
+	  prerr_endline ("CoqIde fatal error:" ^ (Printexc.to_string e));
+	  crash_save 127
+  done
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
index de19db4c3..53d4a020c 100644
--- a/ide/find_phrase.mll
+++ b/ide/find_phrase.mll
@@ -9,8 +9,10 @@ rule next_phrase = parse
 	   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) 
+      { 
+	let c = Lexing.lexeme lexbuf in 
+	if Ideutils.is_char_start c.[0] then incr length; 
+	c^(next_phrase lexbuf) 
       }
   | eof  { raise (Lex_error "no phrase") }
 and skip_comment = parse
@@ -18,5 +20,5 @@ and skip_comment = parse
   | "(*" {incr length; incr length; 
 	  skip_comment lexbuf;
 	  skip_comment lexbuf}
-  | _  { incr length; skip_comment lexbuf}
+  | _  { if Ideutils.is_char_start (Lexing.lexeme lexbuf).[0] then incr length; skip_comment lexbuf}
   | eof  { raise (Lex_error "No closing *)") }
diff --git a/ide/highlight.mll b/ide/highlight.mll
index 8b187c754..e58654714 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -73,3 +73,33 @@ and comment = parse
   | "(*" { ignore (comment lexbuf); comment lexbuf }
   | _    { comment lexbuf }
   | eof  { raise End_of_file }
+
+{
+  open Ideutils
+
+  let highlight_slice (input_buffer:GText.buffer) (start:GText.iter) stop = 
+  let offset = start#offset in
+  let s = start#get_slice ~stop in
+  let convert_pos = byte_offset_to_char_offset s in
+  let lb = Lexing.from_string s in
+    try 
+      while true do
+	process_pending ();
+	let b,e,o=next_order lb in
+	let b,e = convert_pos b,convert_pos e in
+	let start = input_buffer#get_iter_at_char (offset + b) in
+	let stop = input_buffer#get_iter_at_char (offset + e) in
+	  input_buffer#apply_tag_by_name ~start ~stop o 
+      done
+    with End_of_file -> ()
+      | _ -> ()
+
+
+  let highlight_current_line input_buffer = 
+  let i = get_insert input_buffer in
+    highlight_slice input_buffer (i#set_line_offset 0) i
+
+  let highlight_all input_buffer = 
+  highlight_slice input_buffer input_buffer#start_iter input_buffer#end_iter
+
+}
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
new file mode 100644
index 000000000..9999e576b
--- /dev/null
+++ b/ide/ideutils.ml
@@ -0,0 +1,45 @@
+
+let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
+
+let is_char_start c = let code = Char.code c in code < 0x80 || code >= 0xc0
+
+let byte_offset_to_char_offset s byte_offset = 
+  assert (byte_offset < String.length s);
+  let count_delta = ref 0 in
+  for i = 0 to byte_offset do
+    let code = Char.code s.[i] in
+    if code >= 0x80 && code < 0xc0 then incr count_delta
+  done;
+  byte_offset - !count_delta
+
+
+let process_pending () = 
+  while Glib.Main.pending () do 
+    ignore (Glib.Main.iteration false) 
+  done
+
+let debug = ref false
+
+let prerr_endline s =
+  if !debug then  prerr_endline s else ()
+
+let print_id id =
+  prerr_endline ("GOT sig id :"^(string_of_int (Obj.magic id)))
+
+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)