aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-indent.el
Commit message (Collapse)AuthorAge
* Fixed a syntactic recognition function. Should Fix #2819.Gravatar Pierre Courtieu2012-07-05
|
* Fix a bug in coq indet code when at the beginning of a buffer.Gravatar Pierre Courtieu2012-06-14
|
* Trying to minimize the slowness of indentation when no "Proof." isGravatar Pierre Courtieu2012-06-11
| | | | given. Seems to work.
* Fixed an ineficiency in comment detection.Gravatar Pierre Courtieu2012-02-10
|
* Cleaning some code.Gravatar Pierre Courtieu2012-02-01
|
* Quick fix of a regression introduced by my last commit. Looking for aGravatar Pierre Courtieu2012-02-01
| | | | better fix.
* Fixed command end recognition in presence of operators of the form .+Gravatar Pierre Courtieu2012-02-01
| | | | +. is not accepted yet.
* Adapting coq syntax recognition to the future v8.4 behavior of bulletsGravatar Pierre Courtieu2011-12-16
| | | | | (stand-alone commands), which is different of the experiments made until now in coq/trunk.
* 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 21:29:05 +0000