aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-indent.el
Commit message (Collapse)AuthorAge
* Update copyright messages and improve the header of elisp files.Gravatar Erik Martin-Dorel2018-02-21
|
* look for vernac controls before focus bracket, fix for #223Gravatar Paul Steckler2018-01-26
|
* Experimental fix for #220.Gravatar Pierre Courtieu2018-01-15
|
* Fix incorrect uses of defvarGravatar Clément Pit--Claudel2017-03-08
| | | | | | | It didn't really matter that these variables were defined and set to nil during compilation, since we ran compilation in a clean Emacs in --batch mode; it does matter now, however, since package.el compiles PG in the user's currently running Emacs instance.
* Fixing a smal glitch in indentation.Gravatar Pierre Courtieu2016-05-27
|
* Fix #29 + indentation glitch + regexp refactoring.Gravatar Pierre Courtieu2016-01-14
|
* Speeding up indentation (regexp optim).Gravatar Pierre Courtieu2015-12-07
|
* Speeding up indentation.Gravatar Pierre Courtieu2015-12-07
| | | | Dedicated regexp for bullets when searching backward.
* Fixed #15 + more speedup of indentation.Gravatar Pierre Courtieu2015-12-05
| | | | | Experimenting on more regexp and less adhoc searching in the smie lexer. In particular the regexp for bullet seems now capture only real bullets.
* Fixed a bug in script navigation. Updated CHANGEGravatar Pierre Courtieu2015-01-27
|
* removed debug message.Gravatar Pierre Courtieu2014-12-30
|
* fixed indentation (lexing of 'with') + made local coq-load-path.Gravatar Pierre Courtieu2014-12-30
|
* fixed a bug in command parsing for coq, due to recent changes.Gravatar Pierre Courtieu2014-12-24
|
* Supporting more bullets (coq 8.5), like ++ or ++++.Gravatar Pierre Courtieu2014-12-23
|
* Summary: Don't quote lambda expressionsGravatar Stefan Monnier2012-08-30
| | | | | | | | | | | | | | | | * coq/coq-indent.el (coq-indent-inner-regexp): Remove old X-Symbol element. (coq-save-count, coq-proof-count): * obsolete/plastic/plastic.el (plastic-shell-handle-output): * lib/texi-docstring-magic.el (texi-docstring-magic-insert-magic): * lib/pg-dev.el (emacs-lisp-mode-hook): * lib/maths-menu.el (maths-menu-filter-predicate) (maths-menu-tokenise-insert): * lib/holes.el (holes-next): * lego/lego.el (lego-shell-handle-output): * isar/isabelle-system.el (isabelle-docs-menu): * coq/coq.el (coq-compile-command, coq-compile-auto-save) (coq-compile-ignored-directories, coq-load-path-safep) (proof-shell-handle-delayed-output-hook): Don't quote lambda.
* 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 15:10:56 +0000