| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2015-03-09 | Added bug fixes in CHANGES. | Pierre Courtieu | |
| 2015-03-09 | Fixes #503. | Pierre Courtieu | |
| Added a "stop silent" if needed in proof-add-queue. This allows to recover verbosity when an error left the prover in silent mode. | |||
| 2015-03-05 | Fixed stuff in CHANGES. | Pierre Courtieu | |
| 2015-03-05 | Customization variables for modules, section and proof indentation. | Pierre Courtieu | |
| 2015-03-05 | Summary: Fix compile warning on phox-toolbar-entries | David Aspinall | |
| 2015-03-05 | Summary: Fix compile warning on isar-markup-ml | David Aspinall | |
| 2015-03-05 | Fix compile error with make-face | David Aspinall | |
| 2015-03-05 | Summary: Remove obsolete function | David Aspinall | |
| 2015-03-05 | Summary: Build on Mac | David Aspinall | |
| 2015-03-05 | Fix colours for dark backgrounds | David Aspinall | |
| 2015-03-04 | Fixed Proof end/start detection on Proof using ... | Pierre Courtieu | |
| Was making scripting confused. P. | |||
| 2015-03-04 | Fixed compilation issue with previous commit + CHANGE updates. | Pierre Courtieu | |
| 2015-03-03 | Mouse queries. | Pierre Courtieu | |
| If enabled, allows to send queries to coq with (control/shift/control-shift) mouse-1. | |||
| 2015-03-03 | Coqtop always restarted when switching script buffer. | Pierre Courtieu | |
| This comes from Hendrik's compile mode and is actually needed even when this mode is off. When switching scripting buffer, restart the coq shell process, so that it applies local coqtop options. | |||
| 2015-02-24 | Making freeze buffer hace coq-response-more. | Pierre Courtieu | |
| So that shortcuts work from this buffer. + colorizing. | |||
| 2015-02-23 | Typo in last commit. | Pierre Courtieu | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |