aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/nanoPG.ml
Commit message (Collapse)AuthorAge
* Correct some spelling errorsmasterGravatar Benjamin Barenblat2018-07-22
| | | | | | | | | | Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Turning CoqIDE preferences into new style.Gravatar Pierre-Marie Pédrot2015-08-16
|/ | | | | Some old style references remain because all type converters are not implemented yet.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Protecting from a List.nth when applying a command, e.g. C-w, on no CoqIDE ↵Gravatar Hugo Herbelin2014-12-07
| | | | buffer.
* nanoPG: when the cursor moves, scroll to make it appear on screenGravatar Enrico Tassi2014-04-09
|
* nanoPG: takeover keypress only when text view has focusGravatar Enrico Tassi2014-04-09
|
* nanoPG: better copy/pasteGravatar Enrico Tassi2014-03-13
|
* [nanoPG]: emacs like copy/pasteGravatar Enrico Tassi2014-02-17
|
* nanoPG: compete rewriting with more Emacs/PG like featuresGravatar Enrico Tassi2014-01-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It is not possible to add shortcuts with arbitrary modifiers and to save into a state some data, like the line offset for C-n and the killed text for C-k and C-y. If you see that your favorite Emacs/PG shortcut is missing, please tell me! Currently supported shortcuts: C-_ Undo C-g Esc C-s Search C-e Move to end of line M-e Move to end of sentence M-a Move to beginning of sentence C-n Move to next line C-p Move to previous line C-f Forward char C-b Backward char M-f Forward word M-b Backward word C-k Kill untill the end of line M-d Kill next word M-k Kill until sentence end M-DELBACK Kill word before cursor C-d Delete next character C-y Yank killed text back C-c C-RET Go to C-c C-n Advance 1 sentence C-c C-u Retract 1 sentence C-c C-b Advance C-c C-r Restart C-c C-c Stop C-c C-a C-p Print C-c C-a C-c Check C-c C-a C-b About C-c C-a C-a Search About C-c C-a C-o Search Pattern C-c C-a C-l Locate C-c C-a C-RET match template C-x C-s Save C-x C-c Quit C-x C-f Open
* Silence compilation warning by avoiding some deprecated constructs.Gravatar Guillaume Melquiond2013-12-03
|
* Add a (very minimal) Proof General mode to CoqIDEGravatar gareuselesinge2013-08-08
documentation available in the help menu git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16685 85f007b7-540e-0410-9357-904b9bb8a0f7