Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix of previous commit. | Pierre Courtieu | 2010-09-07 |
| | |||
* | half fixed the indentation bug at buffer start. | Pierre Courtieu | 2010-09-07 |
| | |||
* | First fix of bug introduced by the last font-lock fix. Not finished. | Pierre Courtieu | 2010-09-03 |
| | |||
* | Fixed bug #346. Coq code was using proof-ids-to-regexp on regexp | Pierre Courtieu | 2010-09-01 |
| | | | | instead of pure strings. | ||
* | coq-comment-at-point: avoid error if command start not found | David Aspinall | 2010-08-24 |
| | | | | (see Trac #342) | ||
* | Fix compile warning, rearrange docs | David Aspinall | 2009-09-07 |
| | |||
* | Clean whitespace | David Aspinall | 2009-09-05 |
| | |||
* | Remove some old X-Symbol references. | David Aspinall | 2009-09-01 |
| | |||
* | Merge changes from Version4Branch. | David Aspinall | 2008-07-24 |
| | |||
* | Fixed indentation and goal display. | Pierre Courtieu | 2008-01-28 |
| | |||
* | Patch and cleanup for Coq indent code, see ↵ | David Aspinall | 2008-01-25 |
| | | | | http://proofgeneral.inf.ed.ac.uk/trac/ticket/173 | ||
* | Missing paren | David Aspinall | 2008-01-24 |
| | |||
* | Fixes and cleanups for coq-indent-line, see Trac #172 | David Aspinall | 2008-01-24 |
| | |||
* | Remove proof-indent-pad-eol atrocity | David Aspinall | 2007-02-28 |
| | |||
* | typo in coq-indent. | Pierre Courtieu | 2006-09-15 |
| | |||
* | fixed a typo in last correction. | Pierre Courtieu | 2006-09-15 |
| | |||
* | fixed a bug from Stefan Monnier. | Pierre Courtieu | 2006-09-14 |
| | |||
* | cleaning from Stefan Monnier. | Pierre Courtieu | 2006-09-13 |
| | |||
* | cleaning from Stefan Monnier. | Pierre Courtieu | 2006-09-13 |
| | |||
* | Fixed nested comment support for scripting, in xemacs (worked already | Pierre Courtieu | 2006-09-08 |
| | | | | on GNU Emacs). Instanciated proof-parse-function for that... | ||
* | Trying to mae indentation aware of nested comments (to be simplified | Pierre Courtieu | 2006-09-04 |
| | | | | | when xemacs will deal with nested comments). Seems to work, a bit slow. | ||
* | Fixed a small bug in indentation of coq. | Pierre Courtieu | 2006-08-25 |
| | | | | Fixed behavior for making abbrev table (don't if it already exists). | ||
* | fixing a bug introduced lately (coq-save-command-p *needs* two args | Pierre Courtieu | 2006-08-24 |
| | | | | beacause proof-save-command-p needs is so defined). | ||
* | Fixed indentation and font-lock for coq. Better, faster. | Pierre Courtieu | 2006-08-23 |
| | |||
* | Coq indentation small fixes. | Pierre Courtieu | 2006-08-23 |
| | |||
* | fsf emacs compatibilty for symbol-at-point. | Pierre Courtieu | 2006-08-23 |
| | |||
* | removed debug messages from indentation code. | Pierre Courtieu | 2006-07-04 |
| | |||
* | fix the bug for coq indetation of two consecutive comments. Code is | Pierre Courtieu | 2006-07-04 |
| | | | | | ugly, should take the code given by Stefan Monnier and adapt it (it does not indent everything as is). | ||
* | fix a bug in coq indentation (loop). seems to be fixed. I still have a | Pierre Courtieu | 2006-07-04 |
| | | | | problem indenting comments (two consecutive comments: second shifted). | ||
* | moving coq-goal-command-p to indetation code, as from v8.1, goals are | Pierre Courtieu | 2006-07-04 |
| | | | | | | detected by the goal attribute of spans. syntactical goal recognizing is still used in indetation code, and for v8.0 compatibility. I shall remove v8.0 compatibility in some months. | ||
* | added match...with automatic building from atype name. | Pierre Courtieu | 2005-11-07 |
| | | | | Had to correct a bug in proof-shell. | ||
* | Finished making holes.el a real minor-mode. There is a new file | Pierre Courtieu | 2005-02-15 |
| | | | | | | | | | holes-load.el which defines the autoloads (enough of them?). All functions have the prefix "holes-", and offending keyboard shortcuts have been either removed or bound to the minor mode. I made holes-mode minor mode automatically turned on in all proof buffers in coq mode (including shell, script and response buffers as it may be useful to copy paste parts of this buffers into holes). | ||
* | debugged the indentation of coq (bug report of Batsiaan Zapf august | Pierre Courtieu | 2004-08-30 |
| | | | | | 3rd 2004). I found another bug (infinite loop due to an error in coq-back-to-indentation-prevline). | ||
* | added the forall x-symbol to the indent keywords lists. | Pierre Courtieu | 2004-03-30 |
| | |||
* | bug fix in holes (call to proof-indent-line instead of funcall | Pierre Courtieu | 2004-03-15 |
| | | | | indent-line-function). | ||
* | little bug fix in coq-indent.el | Pierre Courtieu | 2004-03-15 |
| | |||
* | bug fixes on indenting and command-end-regexp. | Pierre Courtieu | 2004-03-11 |
| | |||
* | compile warning corrections | Pierre Courtieu | 2004-03-10 |
| | |||
* | indentation for coq completely re-coded, because the generic mechanism | Pierre Courtieu | 2004-03-08 |
does not use "proof-goal-command-p" and is not powerful enough. |