| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-10-16 | Fix #514 + support for named goal selector. | Pierre Courtieu | |
| It was hard to separate this too fixes (same regexps). | |||
| 2020-03-12 | moving tests for monadic notations and Equations in separate files. | Pierre Courtieu | |
| 2020-03-12 | Fix #465: Indentation of Equations (plugin). | Pierre Courtieu | |
| 2020-03-02 | Adding Tests for indentation related to plugins. | Pierre Courtieu | |
| Namely monadic notations and Equations (the latter is bugged currently). | |||
| 2020-01-19 | Generic monadic indentation + specifically ext-lib / Compcert + doc. | Pierre Courtieu | |
| This a generalization of PR#451 proposed by @Chobbes. Since these syntax are not completely universal (and not builtin in coq), the idea is to make the syntax customizable, especially to make it possible to disable it. NOTE: to make the Compcert syntax supported I had to refine the smie lexer so that the ";" token was emitted as a fllback instead of "; tactic". NOTE2: I had to make the coq-user-token and coq-monadic-tokens be tested ON THE RESULT of smie-coq-backward-token. | |||
| 2019-06-17 | fixing with inductive indentation. | Pierre Courtieu | |
| 2017-05-23 | Fixing #183. | Pierre Courtieu | |
| 2017-03-03 | Merge pull request #163 from ProofGeneral/fix_indentation | Pierre Courtieu | |
| Fix indentation | |||
| 2017-03-02 | use Utf8 from Coq library | Paul Steckler | |
| 2017-01-26 | Fixing #147 and #91 + others indentation bugs. | Pierre Courtieu | |
| While fixing these I discovered several flaws in indentation (what a suprise). The probem is the following: since we don't have a precise grammar of tactics, smie often decides that the parent of a sub-part of a tactic is the previous command instead of the current tacic. Typical example (fixed now but in general): foo. apply bar with bar'. Since "apply ... bar'" is considered as one leaf of the grammar, it is considered to be a child of the previous dot. . /\ / \ foo apply...bar' Therefore indentation of "with" wants to align with parent "." and hence with "foo". Basically we should try to define a much more precise grammar of complex tactics (with with, as, using etc) in order to fix the problem. Of course this has the drawback of making impossible to support user tactic notations. | |||
| 2015-03-23 | Fixed lazymatch and multimatch indentation/highlighting. | Pierre Courtieu | |
| 2015-01-05 | Fixing indentation of pending curly braces. | Pierre Courtieu | |
| 2015-01-05 | trying to indent pending forall in the expected way | Pierre Courtieu | |
| 2014-12-30 | fixed indentation (lexing of 'with') + made local coq-load-path. | Pierre Courtieu | |
| 2014-12-24 | fixed a bug in command parsing for coq, due to recent changes. | Pierre Courtieu | |
| 2014-06-06 | * coq/coq-smie.el: Fix precedence of 'else'. | Stefan Monnier | |
| 2014-06-04 | * coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition. | Stefan Monnier | |
| (coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=". | |||
| 2014-06-03 | Rename coq-smie-lexer.el to coq-smie.el. | Stefan Monnier | |
| 2013-07-11 | Fixing another bug in indentation concerning "where". Actually there | Pierre Courtieu | |
| are other uses of "where (declaring notation for records that I did no test). | |||
| 2012-11-13 | - first version of parallel asynchronous compilation for coq in | Hendrik Tews | |
| coq-par-compile.el (must be activated via coq-compile-parallel-in-background) - items in the queue region are not necessarily in proof-action-list any more! Require commands and the following items are stored elsewhere until the compilation finishes. Variable proof-second-action-list-active notifies the generic machinery if queue items are stored elsewhere. In this case, Proof General must neither release the proof shell lock nor delete the queue span when proof-action-list is empty. - to kill background processes as early as possible, the new hook proof-shell-signal-interrupt-hook is used | |||
| 2012-07-10 | Fixed incorrect syntax of previous commit. | Pierre Courtieu | |
| 2012-06-08 | Indentation is a bit more accurate. | Pierre Courtieu | |
| 2012-06-07 | Fix indentation of dependent match clauses (as ... in ... return ...). | Pierre Courtieu | |
| + bug fixes. | |||
| 2012-06-04 | One more fix for indentation. | Pierre Courtieu | |
| 2012-06-03 | Fix a bug of indentation. | Pierre Courtieu | |
| 2012-05-09 | fix typo + add one missing cvsignore | Hendrik Tews | |
| 2012-02-10 | Fixed an ineficiency in comment detection. | Pierre Courtieu | |
| 2011-12-27 | Typo | David Aspinall | |
| 2011-07-08 | Fixing the scripting of new subproof script parenthesizing ({ and }). | Pierre Courtieu | |
| 2011-07-01 | Some more sample indentation patterns added. | Pierre Courtieu | |
| 2011-06-17 | oops, undo last commit. | Pierre Courtieu | |
| 2011-06-10 | Fix trac #410. | Pierre Courtieu | |
| 2011-06-08 | Added one indentation example. | Pierre Courtieu | |
| 2011-06-04 | Updated the old code for indentation, in case Stefan cannot finish the | Pierre Courtieu | |
| 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. | |||
| 2011-05-20 | - minor changes: clean personal todo list + adjust test case description | Hendrik Tews | |
| 2011-05-12 | - add test coq/ex/test-cases/change-ancestor for the | Hendrik Tews | |
| change-ancestor bug | |||
| 2011-02-28 | - adjust coq-ask-insert-coq-prog-name and doc in coq-local-vars-doc | Hendrik Tews | |
| 2011-01-26 | - fix problem description | Hendrik Tews | |
| 2011-01-21 | - use time-less-p | Hendrik Tews | |
| - delete previous-head, simplify loop - coq 8.2 compatibility - describe bug for killing completely asserted active buffers in coq/ex/test-cases/retract-completely-asserted | |||
| 2011-01-18 | - fixed stale load path problem with killing the proof shell in | Hendrik Tews | |
| the deactivation-hook | |||
| 2011-01-17 | fix problems in test cases | Hendrik Tews | |
| coq/ex/test-cases/multiple-files-single-dir and multiple-files-multiple-dir | |||
| 2011-01-14 | - more coq test cases (some with surprising and embarrassing bugs) | Hendrik Tews | |
| 2011-01-14 | - move proof-no-fully-processed-buffer to generic/proof-config | Hendrik Tews | |
| - add documentation for it - add a test case demonstrating it in coq/ex/test-cases/retract-completely-asserted | |||
| 2010-09-09 | Fixed small bugs in indentation. | Pierre Courtieu | |
| 2010-09-08 | illustrating the wrongness of the current multifile processing for coq. | Pierre Courtieu | |
| 2010-09-08 | Added three files for testing multi file scripting. | Pierre Courtieu | |
| 2010-08-15 | Moved files | David Aspinall | |
| 2010-08-13 | Renamed file | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |