coqide: maj preferences du wizzard

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

5 files changed, 120 insertions, 14 deletions

diff --git a/.depend b/.depend
index 8867ab9060..aec3b883eb 100644
--- a/.depend
+++ b/.depend
@@ -1,3 +1,5 @@
+ide.good/coq.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
+    kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 ide/coq.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
     kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 interp/constrextern.cmi: kernel/environ.cmi library/libnames.cmi \
@@ -434,6 +436,7 @@ contrib/linear/unif.cmi: contrib/linear/dpctypes.cmi \
 contrib/xml/doubleTypeInference.cmi: contrib/xml/acic.cmo kernel/environ.cmi \
     pretyping/evd.cmi kernel/term.cmi 
 contrib/xml/xmlcommand.cmi: library/libnames.cmi 
+ide.good/utils/configwin.cmi: ide/utils/uoptions.cmi 
 ide/utils/configwin.cmi: ide/utils/uoptions.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
@@ -455,6 +458,44 @@ 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.good/command_windows.cmo: ide/coq.cmi ide/coq_commands.cmo \
+    ide/ideutils.cmo 
+ide.good/command_windows.cmx: ide/coq.cmx ide/coq_commands.cmx \
+    ide/ideutils.cmx 
+ide.good/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 lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+    pretyping/reductionops.cmi proofs/refiner.cmi library/states.cmi \
+    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi toplevel/vernac.cmi \
+    toplevel/vernacentries.cmi toplevel/vernacexpr.cmo ide.good/coq.cmi 
+ide.good/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx \
+    toplevel/coqtop.cmx kernel/environ.cmx pretyping/evarutil.cmx \
+    pretyping/evd.cmx tactics/hipattern.cmx ide/ideutils.cmx library/lib.cmx \
+    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
+    lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+    pretyping/reductionops.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.good/coq.cmi 
+ide.good/coqide.cmo: ide/command_windows.cmo ide/coq.cmi ide/coq_commands.cmo \
+    ide/find_phrase.cmo ide/highlight.cmo ide/ideutils.cmo proofs/pfedit.cmi \
+    ide/preferences.cmo ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo 
+ide.good/coqide.cmx: ide/command_windows.cmx ide/coq.cmx ide/coq_commands.cmx \
+    ide/find_phrase.cmx ide/highlight.cmx ide/ideutils.cmx proofs/pfedit.cmx \
+    ide/preferences.cmx ide/undo.cmx lib/util.cmx toplevel/vernacexpr.cmx 
+ide.good/find_phrase.cmo: ide/ideutils.cmo 
+ide.good/find_phrase.cmx: ide/ideutils.cmx 
+ide.good/highlight.cmo: ide/ideutils.cmo 
+ide.good/highlight.cmx: ide/ideutils.cmx 
+ide.good/ideutils.cmo: config/coq_config.cmi lib/options.cmi \
+    lib/pp_control.cmi ide/preferences.cmo 
+ide.good/ideutils.cmx: config/coq_config.cmx lib/options.cmx \
+    lib/pp_control.cmx ide/preferences.cmx 
+ide.good/preferences.cmo: ide/utils/configwin.cmi 
+ide.good/preferences.cmx: ide/utils/configwin.cmx 
+ide.good/undo.cmo: ide/ideutils.cmo ide.good/undo.cmi 
+ide.good/undo.cmx: ide/ideutils.cmx ide.good/undo.cmi 
 ide/command_windows.cmo: ide/coq.cmi ide/coq_commands.cmo ide/ideutils.cmo 
 ide/command_windows.cmx: ide/coq.cmx ide/coq_commands.cmx ide/ideutils.cmx 
 ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
@@ -487,8 +528,8 @@ ide/ideutils.cmo: config/coq_config.cmi lib/options.cmi lib/pp_control.cmi \
     ide/preferences.cmo 
 ide/ideutils.cmx: config/coq_config.cmx lib/options.cmx lib/pp_control.cmx \
     ide/preferences.cmx 
-ide/preferences.cmo: ide/utils/configwin.cmi 
-ide/preferences.cmx: ide/utils/configwin.cmx 
+ide/preferences.cmo: ide/utils/configwin.cmi ide/utils/editable_cells.cmo 
+ide/preferences.cmx: ide/utils/configwin.cmx ide/utils/editable_cells.cmx 
 ide/undo.cmo: ide/ideutils.cmo ide/undo.cmi 
 ide/undo.cmx: ide/ideutils.cmx ide/undo.cmi 
 interp/constrextern.cmo: pretyping/classops.cmi library/declare.cmi \
@@ -3229,6 +3270,28 @@ 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 
+ide.good/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
+    ide/utils/configwin_types.cmo ide.good/utils/configwin.cmi 
+ide.good/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
+    ide/utils/configwin_types.cmx ide.good/utils/configwin.cmi 
+ide.good/utils/configwin_html_config.cmo: ide/utils/configwin_ihm.cmo \
+    ide/utils/configwin_messages.cmo ide/utils/configwin_types.cmo \
+    ide/utils/uoptions.cmi 
+ide.good/utils/configwin_html_config.cmx: ide/utils/configwin_ihm.cmx \
+    ide/utils/configwin_messages.cmx ide/utils/configwin_types.cmx \
+    ide/utils/uoptions.cmx 
+ide.good/utils/configwin_ihm.cmo: ide/utils/configwin_messages.cmo \
+    ide/utils/configwin_types.cmo ide/utils/okey.cmi ide/utils/uoptions.cmi 
+ide.good/utils/configwin_ihm.cmx: ide/utils/configwin_messages.cmx \
+    ide/utils/configwin_types.cmx ide/utils/okey.cmx ide/utils/uoptions.cmx 
+ide.good/utils/configwin_types.cmo: ide/utils/configwin_keys.cmo \
+    ide/utils/uoptions.cmi 
+ide.good/utils/configwin_types.cmx: ide/utils/configwin_keys.cmx \
+    ide/utils/uoptions.cmx 
+ide.good/utils/okey.cmo: ide.good/utils/okey.cmi 
+ide.good/utils/okey.cmx: ide.good/utils/okey.cmi 
+ide.good/utils/uoptions.cmo: ide.good/utils/uoptions.cmi 
+ide.good/utils/uoptions.cmx: ide.good/utils/uoptions.cmi 
 ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
     ide/utils/configwin_types.cmo ide/utils/configwin.cmi 
 ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
diff --git a/INSTALL.ide b/INSTALL.ide
index d6a91f3d8e..ff5088dc49 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -26,21 +26,21 @@ REQUIREMENT:
 INSTALLATION
  1) You need to install the OCaml stub library lablgtk2. See 
        		http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
-	  The official snapshot are not yet ready for CoqIde.
+	  The first official beta snapshot is needed.
 	  Use this one :
-		http://www.lix.polytechnique.fr/~monate/download/lablgtk2.tgz
+http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk2-beta.tar.gz
     If you are in a hurry just run :
     
     cd /tmp && \
-    wget http://www.lix.polytechnique.fr/~monate/download/lablgtk2.tgz && \
-    tar zxvf lablgtk2.tgz && \
-    cd lablgtk2 && \
+    wget http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk2-beta.tar.gz && \
+    tar zxvf lablgtk2-beta.tar.gz && \
+    cd lablgtk2-beta && \
     make configure && \
     make all opt && \
     make install
 
    You must have write access to the OCaml standard library path.
-   If this fails read lablgtk2/README.
+   If this fails read lablgtk2-beta/README.
 
 2) Go into your Coq source directory and then : 
 
@@ -53,3 +53,4 @@ Font configuration is not saved.
 If you want to change the defaults fonts, just copy the
 .coqiderc file located in the ide subdir of the Coq library to
 your home directory and edit it by hand.
+Read ide/FAQ for more informations.
diff --git a/Makefile b/Makefile
index 006ffaf224..7aadc0a08f 100644
--- a/Makefile
+++ b/Makefile
@@ -366,7 +366,9 @@ COQIDE=bin/coqide.$(BEST)$(EXE)
 COQIDECMO=ide/utils/okey.cmo ide/utils/uoptions.cmo \
 	  ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo \
 	  ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmo \
-	  ide/utils/configwin.cmo ide/config_lexer.cmo ide/preferences.cmo \
+	  ide/utils/configwin.cmo \
+	  ide/utils/editable_cells.cmo ide/config_lexer.cmo \
+	  ide/preferences.cmo \
 	  ide/ideutils.cmo ide/undo.cmo \
 	  ide/find_phrase.cmo \
           ide/highlight.cmo ide/coq.cmo ide/coq_commands.cmo \
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 51c7a025cc..c78cf32140 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -294,11 +294,15 @@ let configure () =
     string ~f:(fun s -> !current.library_url <- s) "Library URL"  !current.library_url in
 
   let automatic_tactics = 
-    list 
-      ~titles:["Coq Command to try";"Coq Command to insert in script"]
-      "Wizzard tactics to apply"
-      (fun (c,i) -> [c;i])
-      !current.automatic_tactics
+    let box = GPack.hbox () in
+    let w = Editable_cells.create !current.automatic_tactics in
+    box#pack w#coerce;
+    custom
+      ~label:"Wizzard tactics to try in order (WORK IN PROGRESS)"
+      box
+      (fun () -> ())
+      true
+
   in
   let cmds =
     [Section("Commands",
diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml
new file mode 100644
index 0000000000..edc9d2b065
--- /dev/null
+++ b/ide/utils/editable_cells.ml
@@ -0,0 +1,36 @@
+let create l = 
+  let hbox = GPack.hbox () in
+  let columns = new GTree.column_list in
+  let command_col =  columns#add GTree.Data.string in
+  let coq_col = columns#add GTree.Data.string in
+  let store = GTree.list_store columns
+  in 
+(* populate the store *)
+  let _ = List.iter (fun (x,y) -> 
+		       let row = store#append () in
+		       store#set ~row ~column:command_col x;
+		       store#set ~row ~column:coq_col y)
+	    l
+  in
+  let view = GTree.view ~model:store ~packing:hbox#pack () in
+  
+  let renderer = GTree.cell_renderer_text () in
+  GtkText.Tag.set_property renderer (`EDITABLE true);
+  let first = 
+    GTree.view_column ~title:"Coq Command to try" 
+      ~renderer:(renderer,["text",command_col]) 
+      () 
+  in ignore (view#append_column first);
+  let second = 
+    GTree.view_column ~title:"Coq Command to insert" 
+      ~renderer:(renderer,["text",coq_col]) 
+      () 
+  in ignore (view#append_column second);
+
+  let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack () in
+  let up = GButton.button ~label:"Up" ~packing:(vbox#pack ~expand:true ~fill:false) () in
+  let down = GButton.button ~label:"Down" ~packing:(vbox#pack ~expand:true ~fill:false) () in
+  let add = GButton.button ~label:"Add" ~packing:(vbox#pack ~expand:true ~fill:false) () in
+  let remove = GButton.button ~label:"Remove" ~packing:(vbox#pack ~expand:true ~fill:false) () in
+  hbox
+