aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-indent.el
Commit message (Collapse)AuthorAge
* Fix trac #420 indentation freezing.Gravatar Pierre Courtieu2011-09-04
|
* Crude patch for Trac #416. I haven't tried to understand indent code fully, ↵Gravatar David Aspinall2011-08-23
| | | | so may not be best fix.
* Fixing the scripting of new subproof script parenthesizing ({ and }).Gravatar Pierre Courtieu2011-07-08
|
* Removed { and } as command terminators for now.Gravatar Pierre Courtieu2011-06-19
| | | | Fixes #412.
* Fix trac #410.Gravatar Pierre Courtieu2011-06-10
|
* Fix compile errors (seems to be code duplication between coq.el and coq-indent)Gravatar David Aspinall2011-06-09
|
* 2011-06-07 Stefan Monnier <monnier@iro.umontreal.ca>Gravatar Stefan Monnier2011-06-07
| | | | | | | | | | | | | * coq/coq.el: Match Proof...Qed and fix ;-vs-| precedence. (coq-smie-grammar): Add ; and | tacticals. Rename decls => cmds. Add CoInductive, and Proof..Qed. (coq-smie-search-token-forward): Rename from coq-smie-search-token; make it more robust. (coq-smie-search-token-backward): New function. (coq-smie-forward-token, coq-smie-backward-token): Use it to distinguish Inductive's ":=" from other uses. (coq-smie-rules): Use smie-rule-separator for |. Add ugly hack for Qed without matching "Proof".
* Updated the old code for indentation, in case Stefan cannot finish theGravatar Pierre Courtieu2011-06-04
| | | | | | | new one for the release. Added also support for an experimental syntax modification: { .. } is a new syntax for Beginsubproof. ... EndSubproof. There a also few minor behavior changes. The code has changed a lot though.
* Some small fixes in indentation for coq.Gravatar Pierre Courtieu2011-05-31
|
* Added indentation for BeginSubProof/EndSubProof.Gravatar Pierre Courtieu2011-05-31
| | | | + added some tactics syntax.
* Fixed the cleaning of goals buffer when proof completedGravatar Pierre Courtieu2010-09-09
| | | | + fixed the refreshing of modeline goal number display.
* Cleaning indentation code.Gravatar Pierre Courtieu2010-09-09
|
* Fixed indentation at end of file.Gravatar Pierre Courtieu2010-09-09
|
* Fixed small bugs in indentation.Gravatar Pierre Courtieu2010-09-09
|
* Finished fixing the small indentation bug at buffer top.Gravatar Pierre Courtieu2010-09-07
|
* Fix of previous commit.Gravatar Pierre Courtieu2010-09-07
|
* half fixed the indentation bug at buffer start.Gravatar Pierre Courtieu2010-09-07
|
* First fix of bug introduced by the last font-lock fix. Not finished.Gravatar Pierre Courtieu2010-09-03
|
* Fixed bug #346. Coq code was using proof-ids-to-regexp on regexpGravatar Pierre Courtieu2010-09-01
| | | | instead of pure strings.
* coq-comment-at-point: avoid error if command start not foundGravatar David Aspinall2010-08-24
| | | | (see Trac #342)
* Fix compile warning, rearrange docsGravatar David Aspinall2009-09-07
|
* Clean whitespaceGravatar David Aspinall2009-09-05
|
* Remove some old X-Symbol references.Gravatar David Aspinall2009-09-01
|
* Merge changes from Version4Branch.Gravatar David Aspinall2008-07-24
|
* Fixed indentation and goal display.Gravatar Pierre Courtieu2008-01-28
|
* Patch and cleanup for Coq indent code, see ↵Gravatar David Aspinall2008-01-25
| | | | http://proofgeneral.inf.ed.ac.uk/trac/ticket/173
* Missing parenGravatar David Aspinall2008-01-24
|
* Fixes and cleanups for coq-indent-line, see Trac #172Gravatar David Aspinall2008-01-24
|
* Remove proof-indent-pad-eol atrocityGravatar David Aspinall2007-02-28
|
* typo in coq-indent.Gravatar Pierre Courtieu2006-09-15
|
* fixed a typo in last correction.Gravatar Pierre Courtieu2006-09-15
|
* fixed a bug from Stefan Monnier.Gravatar Pierre Courtieu2006-09-14
|
* cleaning from Stefan Monnier.Gravatar Pierre Courtieu2006-09-13
|
* cleaning from Stefan Monnier.Gravatar Pierre Courtieu2006-09-13
|
* Fixed nested comment support for scripting, in xemacs (worked alreadyGravatar Pierre Courtieu2006-09-08
| | | | on GNU Emacs). Instanciated proof-parse-function for that...
* Trying to mae indentation aware of nested comments (to be simplifiedGravatar Pierre Courtieu2006-09-04
| | | | | when xemacs will deal with nested comments). Seems to work, a bit slow.
* Fixed a small bug in indentation of coq.Gravatar Pierre Courtieu2006-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 argsGravatar Pierre Courtieu2006-08-24
| | | | beacause proof-save-command-p needs is so defined).
* Fixed indentation and font-lock for coq. Better, faster.Gravatar Pierre Courtieu2006-08-23
|
* Coq indentation small fixes.Gravatar Pierre Courtieu2006-08-23
|
* fsf emacs compatibilty for symbol-at-point.Gravatar Pierre Courtieu2006-08-23
|
* removed debug messages from indentation code.Gravatar Pierre Courtieu2006-07-04
|
* fix the bug for coq indetation of two consecutive comments. Code isGravatar Pierre Courtieu2006-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 aGravatar Pierre Courtieu2006-07-04
| | | | problem indenting comments (two consecutive comments: second shifted).
* moving coq-goal-command-p to indetation code, as from v8.1, goals areGravatar Pierre Courtieu2006-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.Gravatar Pierre Courtieu2005-11-07
| | | | Had to correct a bug in proof-shell.
* Finished making holes.el a real minor-mode. There is a new fileGravatar Pierre Courtieu2005-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 augustGravatar Pierre Courtieu2004-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.Gravatar Pierre Courtieu2004-03-30
|
* bug fix in holes (call to proof-indent-line instead of funcallGravatar Pierre Courtieu2004-03-15
| | | | indent-line-function).
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 09:31:10 +0000