CoqIDEWishes

Wish list for COQIDE

The purpose of this page is to list wishes for CoqIDE and to set priorities.

Use default bindings compatible with most major platforms (e.g. Forward and Backward default key bindings Ctrl-Alt-Up/Down are unavailable under Gnome).
F4/F5 query features better delimiting ident (taking qualified names, ' and _ under consideration).
F4/F5 query features not forcing a selection in the clipboard.
More user-friendly completion (without needing to type a neutral key to keep the completion or use a shortcut to complete).
Uniform behavior of copy-pasting between windows Done in trunk.
Replacing the not-often-used output windows by something using less work space?

Have a fully customizable colors set (in the 8.4 version I had to modify by hand "ide/tags.ml" to have my own set of colors).

At the time this is written, you can modify "coqide-gtk2rc" in your xdg directory, but that only changes the background of the window, not the "light green" background of the already read part. This make this unusable for "dark themes" since in those themes, the background is dark whereas the foreground is light; as a result, you will end up with "light foreground" on "light green background" and it is barely readable. I guess a patch to read a configuration file for colors (maybe merge it with coqiderc; or better would be to use the coqide-gtk2rc file, but I am not a gtk pro, so I don't know how to do it) at startup should be easy to do; having a tab in the preference window would be even better, but longer to do.

Proofs scripts folding Done by V. Gross in trunk, feedback welcome.
Print the current number a goals somewhere which is not subject to scrolling (number of goals should be always visible)
Displays hypotheses and goal in two separate panes?
Search/replace could be a pane at the bottom as in firefox (not a window)
Search/replace could have the same semantics/shortcuts as in emacs
A graphical advanced search windows for driving SearchAbout.
--A small detail: when after scrolling down in a fresh coqide we click inside the buffer, it brings back the pointer to the top instead putting it at the current location-- now ok

Easier support for Unicode (support for some input method, e.g. writing \forall automatically display ∀). (Granted by V. Gross, then A. Charguéraud)
Ltac debugging à la coquille (https://code.google.com/p/coquille/) (by J. Fehrle)
--Allow editing buffer (only the white part) during evaluation-- provided by E. Tassi
--Allow modifying comments (even in the green part) without re-evaluating the buffer-- partly provided by E. Tassi
--Allow changing the target of evaluation (the scope of the blue part) during evaluation-- now ok
Robustness, especially in Windows, thanks to a move from a GTK-thread-based interface to a process-based interface (Vincent Gross, 2009, Pierre Letouzey)