Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix most doc issues raised by (checkdoc) | 2018-08-23 | |
| | |||
* | Update copyright messages and improve the header of elisp files. | 2018-02-21 | |
| | |||
* | look for vernac controls before focus bracket, fix for #223 | 2018-01-26 | |
| | |||
* | Experimental fix for #220. | 2018-01-15 | |
| | |||
* | Fix incorrect uses of defvar | 2017-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. | 2016-05-27 | |
| | |||
* | Fix #29 + indentation glitch + regexp refactoring. | 2016-01-14 | |
| | |||
* | Speeding up indentation (regexp optim). | 2015-12-07 | |
| | |||
* | Speeding up indentation. | 2015-12-07 | |
| | | | | Dedicated regexp for bullets when searching backward. | ||
* | Fixed #15 + more speedup of indentation. | 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 | 2015-01-27 | |
| | |||
* | removed debug message. | 2014-12-30 | |
| | |||
* | fixed indentation (lexing of 'with') + made local coq-load-path. | 2014-12-30 | |
| | |||
* | fixed a bug in command parsing for coq, due to recent changes. | 2014-12-24 | |
| | |||
* | Supporting more bullets (coq 8.5), like ++ or ++++. | 2014-12-23 | |
| | |||
* | Summary: Don't quote lambda expressions | 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. | 2012-07-05 | |
| | |||
* | Fix a bug in coq indet code when at the beginning of a buffer. | 2012-06-14 | |
| | |||
* | Trying to minimize the slowness of indentation when no "Proof." is | 2012-06-11 | |
| | | | | given. Seems to work. | ||
* | Fixed an ineficiency in comment detection. | 2012-02-10 | |
| | |||
* | Cleaning some code. | 2012-02-01 | |
| | |||
* | Quick fix of a regression introduced by my last commit. Looking for a | 2012-02-01 | |
| | | | | better fix. | ||
* | Fixed command end recognition in presence of operators of the form .+ | 2012-02-01 | |
| | | | | +. is not accepted yet. | ||
* | Adapting coq syntax recognition to the future v8.4 behavior of bullets | 2011-12-16 | |
| | | | | | (stand-alone commands), which is different of the experiments made until now in coq/trunk. | ||
* | Fix trac #420 indentation freezing. | 2011-09-04 | |
| | |||
* | Crude patch for Trac #416. I haven't tried to understand indent code fully, ↵ | 2011-08-23 | |
| | | | | so may not be best fix. | ||
* | Fixing the scripting of new subproof script parenthesizing ({ and }). | 2011-07-08 | |
| | |||
* | Removed { and } as command terminators for now. | 2011-06-19 | |
| | | | | Fixes #412. | ||
* | Fix trac #410. | 2011-06-10 | |
| | |||
* | Fix compile errors (seems to be code duplication between coq.el and coq-indent) | 2011-06-09 | |
| | |||
* | 2011-06-07 Stefan Monnier <monnier@iro.umontreal.ca> | 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 | 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. | 2011-05-31 | |
| | |||
* | Added indentation for BeginSubProof/EndSubProof. | 2011-05-31 | |
| | | | | + added some tactics syntax. | ||
* | Fixed the cleaning of goals buffer when proof completed | 2010-09-09 | |
| | | | | + fixed the refreshing of modeline goal number display. | ||
* | Cleaning indentation code. | 2010-09-09 | |
| | |||
* | Fixed indentation at end of file. | 2010-09-09 | |
| | |||
* | Fixed small bugs in indentation. | 2010-09-09 | |
| | |||
* | Finished fixing the small indentation bug at buffer top. | 2010-09-07 | |
| | |||
* | Fix of previous commit. | 2010-09-07 | |
| | |||
* | half fixed the indentation bug at buffer start. | 2010-09-07 | |
| | |||
* | First fix of bug introduced by the last font-lock fix. Not finished. | 2010-09-03 | |
| | |||
* | Fixed bug #346. Coq code was using proof-ids-to-regexp on regexp | 2010-09-01 | |
| | | | | instead of pure strings. | ||
* | coq-comment-at-point: avoid error if command start not found | 2010-08-24 | |
| | | | | (see Trac #342) | ||
* | Fix compile warning, rearrange docs | 2009-09-07 | |
| | |||
* | Clean whitespace | 2009-09-05 | |
| | |||
* | Remove some old X-Symbol references. | 2009-09-01 | |
| | |||
* | Merge changes from Version4Branch. | 2008-07-24 | |
| | |||
* | Fixed indentation and goal display. | 2008-01-28 | |
| | |||
* | Patch and cleanup for Coq indent code, see ↵ | 2008-01-25 | |
| | | | | http://proofgeneral.inf.ed.ac.uk/trac/ticket/173 |