diff options
| -rw-r--r-- | .depend | 67 | ||||
| -rw-r--r-- | INSTALL.ide | 13 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | ide/preferences.ml | 14 | ||||
| -rw-r--r-- | ide/utils/editable_cells.ml | 36 |
5 files changed, 120 insertions, 14 deletions
@@ -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 d6a91f3d8..ff5088dc4 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. @@ -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 51c7a025c..c78cf3214 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 000000000..edc9d2b06 --- /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 + |