Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fixing a smal glitch in indentation. | Pierre Courtieu | 2016-05-27 |
| | |||
* | Fix #29 + indentation glitch + regexp refactoring. | Pierre Courtieu | 2016-01-14 |
| | |||
* | Speeding up indentation (regexp optim). | Pierre Courtieu | 2015-12-07 |
| | |||
* | Speeding up indentation. | Pierre Courtieu | 2015-12-07 |
| | | | | Dedicated regexp for bullets when searching backward. | ||
* | Fixed #15 + more speedup of indentation. | Pierre Courtieu | 2015-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 CHANGE | Pierre Courtieu | 2015-01-27 |
| | |||
* | removed debug message. | Pierre Courtieu | 2014-12-30 |
| | |||
* | fixed indentation (lexing of 'with') + made local coq-load-path. | Pierre Courtieu | 2014-12-30 |
| | |||
* | fixed a bug in command parsing for coq, due to recent changes. | Pierre Courtieu | 2014-12-24 |
| | |||
* | Supporting more bullets (coq 8.5), like ++ or ++++. | Pierre Courtieu | 2014-12-23 |
| | |||
* | Summary: Don't quote lambda expressions | Stefan Monnier | 2012-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. | Pierre Courtieu | 2012-07-05 |
| | |||
* | Fix a bug in coq indet code when at the beginning of a buffer. | Pierre Courtieu | 2012-06-14 |
| | |||
* | Trying to minimize the slowness of indentation when no "Proof." is | Pierre Courtieu | 2012-06-11 |
| | | | | given. Seems to work. | ||
* | Fixed an ineficiency in comment detection. | Pierre Courtieu | 2012-02-10 |
| | |||
* | Cleaning some code. | Pierre Courtieu | 2012-02-01 |
| | |||
* | Quick fix of a regression introduced by my last commit. Looking for a | Pierre Courtieu | 2012-02-01 |
| | | | | better fix. | ||
* | Fixed command end recognition in presence of operators of the form .+ | Pierre Courtieu | 2012-02-01 |
| | | | | +. is not accepted yet. | ||
* | Adapting coq syntax recognition to the future v8.4 behavior of bullets | Pierre Courtieu | 2011-12-16 |
| | | | | | (stand-alone commands), which is different of the experiments made until now in coq/trunk. | ||
* | Fix trac #420 indentation freezing. | Pierre Courtieu | 2011-09-04 |
| | |||
* | Crude patch for Trac #416. I haven't tried to understand indent code fully, ↵ | David Aspinall | 2011-08-23 |
| | | | | so may not be best fix. | ||
* | Fixing the scripting of new subproof script parenthesizing ({ and }). | Pierre Courtieu | 2011-07-08 |
| | |||
* | Removed { and } as command terminators for now. | Pierre Courtieu | 2011-06-19 |
| | | | | Fixes #412. | ||
* | Fix trac #410. | Pierre Courtieu | 2011-06-10 |
| | |||
* | Fix compile errors (seems to be code duplication between coq.el and coq-indent) | David Aspinall | 2011-06-09 |
| | |||
* | 2011-06-07 Stefan Monnier <monnier@iro.umontreal.ca> | Stefan Monnier | 2011-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 the | Pierre Courtieu | 2011-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. | Pierre Courtieu | 2011-05-31 |
| | |||
* | Added indentation for BeginSubProof/EndSubProof. | Pierre Courtieu | 2011-05-31 |
| | | | | + added some tactics syntax. | ||
* | Fixed the cleaning of goals buffer when proof completed | Pierre Courtieu | 2010-09-09 |
| | | | | + fixed the refreshing of modeline goal number display. | ||
* | Cleaning indentation code. | Pierre Courtieu | 2010-09-09 |
| | |||
* | Fixed indentation at end of file. | Pierre Courtieu | 2010-09-09 |
| | |||
* | Fixed small bugs in indentation. | Pierre Courtieu | 2010-09-09 |
| | |||
* | Finished fixing the small indentation bug at buffer top. | Pierre Courtieu | 2010-09-07 |
| | |||
* | 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 |
| |