| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-09-25 | More Fixes when issuing commands from another buffer. | Pierre Courtieu | |
| 2015-09-25 | Fixed bug when issuing commands from another buffer than scripting one. | Pierre Courtieu | |
| Hooks modifying things in *goals* or *response* now try to operate on the right frame/windows. | |||
| 2015-09-22 | hyps highlighting now supports compact contexts (in coq trunk soon). | Pierre Courtieu | |
| 2015-06-23 | Added a moderate support for double quotes in -arg lines of _CoqProject. | Pierre Courtieu | |
| 2015-06-23 | Update to CHANGE. | Pierre Courtieu | |
| 2015-05-19 | robustify last commit (disabling smie show-paren). | Pierre Courtieu | |
| 2015-05-19 | Disable smie parenthesis blink. Too slow sometimes. | Pierre Courtieu | |
| 2015-05-07 | Fixes #492. fixed regexp (\\< --> \\_< everywhere). | Pierre Courtieu | |
| Surprising that this did not raise before... | |||
| 2015-05-07 | Fixes #484. Added syntax. | Pierre Courtieu | |
| 2015-05-07 | Fixes #485. | Pierre Courtieu | |
| 2015-05-07 | Fixes #486 with an option. | Pierre Courtieu | |
| 2015-05-07 | Yet another half fix of smie lexer. | Pierre Courtieu | |
| || is either a boolean operator or a tactical. | |||
| 2015-04-27 | Fixed at-point detection (bis). | Pierre Courtieu | |
| 2015-04-27 | Fixed at-point detection. | Pierre Courtieu | |
| 2015-04-14 | bold unicode biders + Fixing highlighting in goals and response buffers + ↵ | Pierre Courtieu | |
| cleaning. | |||
| 2015-04-13 | Debugging font-lock for ∀, ∃, and λ. | Pierre Courtieu | |
| 2015-04-10 | Added unicode forall in font-lock regexps. | Pierre Courtieu | |
| 2015-04-07 | Added comment. | Pierre Courtieu | |
| 2015-04-07 | Fixed coq-id definition to be correct wrt to coq grammar. | Pierre Courtieu | |
| 2015-04-07 | Fixed highlighting of evars. | Pierre Courtieu | |
| 2015-04-03 | Trying to prepare indentation cleaning... | Pierre Courtieu | |
| 2015-04-02 | Highlighting stuff in goals mode (C-c C-a C-h). Very basic for now. | Pierre Courtieu | |
| 2015-04-01 | Fix fill-paragraph merging comments and code (never fill code). | Pierre Courtieu | |
| 2015-03-31 | Fixed smie code for ";" + added || in grammar. | Pierre Courtieu | |
| Actually || and + are overloaded and I don"t see how to deambiguate them. Indetation may be buggy until I found away. | |||
| 2015-03-27 | Fixed a small bug in indentation. | Pierre Courtieu | |
| 2015-03-27 | Fix disable evar colorizing in coq file. | Pierre Courtieu | |
| 2015-03-27 | Fixed a regex for detecting ids at point. | Pierre Courtieu | |
| 2015-03-26 | Colorizing hyps names robustified. Still incomplete. | Pierre Courtieu | |
| 2015-03-26 | A command to set coq printing width smartly. | Pierre Courtieu | |
| Set the width to the current goals window. Default binding: C-c C-a C-w. | |||
| 2015-03-26 | A remark about project file in the documentation. | Pierre Courtieu | |
| Saying that one -arg should be followed by only one option. For several options, put several -arg, ONE PER LINE. | |||
| 2015-03-26 | Fixed a smal bug in colorizing response buffer. | Pierre Courtieu | |
| First constructor of an inductive was colorized as a hyp name. Hyp name colorizing should be done another way. Using font-lock here is probably bad. | |||
| 2015-03-24 | Fixed indetation of tryif then else. | Pierre Courtieu | |
| 2015-03-24 | fixed gfail hilighting. | Pierre Courtieu | |
| 2015-03-24 | added some keywords | Pierre Courtieu | |
| 2015-03-23 | Highlighting evars. | Pierre Courtieu | |
| 2015-03-23 | Fixed lazymatch and multimatch indentation/highlighting. | Pierre Courtieu | |
| 2015-03-13 | Summary: remove non-BSD cp arg | David Aspinall | |
| 2015-03-13 | Update dates for release next month | David Aspinall | |
| 2015-03-13 | Summary: Experimental Dockerfile | David Aspinall | |
| 2015-03-13 | Set version tag for new release. | David Aspinall | |
| 2015-03-13 | Summary: FAQ about copying output into new buffers | David Aspinall | |
| 2015-03-13 | Summary: Fix to work with dark color themes (stipple with header-line face) | David Aspinall | |
| 2015-03-13 | Summary: Compile warning on speedbar-add-supported-extension | David Aspinall | |
| 2015-03-13 | Summary: Fix for bug #489 (make p-electric-terminator-enable appear as minor ↵ | David Aspinall | |
| mode) | |||
| 2015-03-13 | Some comments for future work. | Pierre Courtieu | |
| 2015-03-13 | Summary: Revert change to default EMACS | David Aspinall | |
| 2015-03-13 | (fixes last commit) Added a command to send Queries to coq, with completion ↵ | Pierre Courtieu | |
| (C-c C-a C-q). Should replace C-c C-v at some point. Needs to have a complete list of such queries. Obeys C-u prefix for Printing all flag. | |||
| 2015-03-13 | Added a command to send Queries to coq, with completion (C-c C-a C-q). | Pierre Courtieu | |
| Should replace C-c C-v at some point. Needs to have a complete list of such queries. Obeys C-u prefix for Printing all flag. | |||
| 2015-03-11 | Summary: Update version year | David Aspinall | |
| 2015-03-11 | Summary: Build in default path for Isabelle2014 Mac package | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |