| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-23 | Fix some typos in comments. | Guillaume Melquiond | |
| 2015-02-20 | Fixing bug #4073. | Pierre-Marie Pédrot | |
| 2015-02-17 | Remove Whelp commands. | Maxime Dénès | |
| Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive. | |||
| 2015-02-17 | Fixing bug #4023 again. | Pierre-Marie Pédrot | |
| 2015-02-17 | Tentative fix for bug #2855. | Pierre-Marie Pédrot | |
| 2015-02-17 | CoqIDE: read-only Qed sentence reflected in colors (Close: 4051) | Enrico Tassi | |
| 2015-02-15 | Fixing bug #4037. | Pierre-Marie Pédrot | |
| 2015-02-15 | Changing default for CoqIDE project to append arguments. | Pierre-Marie Pédrot | |
| Implement wish #3582. | |||
| 2015-02-15 | CoqIDE now remembers the path of the last opened project. | Pierre-Marie Pédrot | |
| Fixes bug #2762. | |||
| 2015-02-15 | Selecting whole words on double-click in CoqIDE. | Pierre-Marie Pédrot | |
| Fixes bug #4026. | |||
| 2015-02-14 | CoqIDE: restore old default colors | Enrico Tassi | |
| 2015-02-14 | Attempt to be more colorblind friendly in CoqIDE (Close #4024) | Enrico Tassi | |
| 2015-02-13 | Fixup version & copyright for MacOS bundle | Pierre Boutillier | |
| 2015-02-13 | Hardcode how coqide have to look for coqtop in MacOS bundle | Pierre Boutillier | |
| Sorry, that is ugly. Please revert if you see a better way to do it. | |||
| 2015-02-13 | Selection of the current word in CoqIDE looks at all buffers. | Pierre-Marie Pédrot | |
| 2015-02-13 | Trying to fix bug #3930. | Pierre-Marie Pédrot | |
| Instead of setting the last modified part of the text to be the insert point, we register all modifications to the buffer between to user actions and take the last modified point to be the least offset of all those modifications. | |||
| 2015-02-12 | Tentative fix for CoqIDE randomly dropping deletions. | Pierre-Marie Pédrot | |
| We make the deletion callback not to regenerate a task id, as the insertion callback does. I can't find a particular reason for this dissymetry, and it was indeed causing trouble. | |||
| 2015-02-12 | Fixing bug #3261. | Pierre-Marie Pédrot | |
| 2015-02-12 | Focussing on message view in CoqIDE when a message is pushed. | Pierre-Marie Pédrot | |
| Also fixes bug #4030. | |||
| 2015-02-12 | Fixing bug #4023. | Pierre-Marie Pédrot | |
| 2015-02-11 | Reinstauring backtrace display in CoqIDE. | Pierre-Marie Pédrot | |
| 2015-02-10 | Making undo/redo atomic in CoqIDE. | Pierre-Marie Pédrot | |
| 2015-02-06 | More efficient Richpp. | Pierre-Marie Pédrot | |
| We build the rich XML at once without generating the printed string. | |||
| 2015-02-04 | Fixing bug #3996. | Pierre-Marie Pédrot | |
| 2015-01-29 | Made the CoqIDE progress gutter clickable. | Pierre-Marie Pédrot | |
| 2015-01-25 | Made replacing of text in CoqIDE atomic w.r.t. the undo/redo. | Pierre-Marie Pédrot | |
| 2015-01-25 | Fixing bug #3947. | Pierre-Marie Pédrot | |
| 2015-01-14 | CoqIDE: a Make file to build coqidetop toploop | Enrico Tassi | |
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2015-01-05 | Removing GUtil dependency from ide/document.ml. | Pierre-Marie Pédrot | |
| We reimplement a quick-n-dirty Gtk-free signal handler. | |||
| 2015-01-05 | Adding an option to deactivate the progress bar. | Pierre-Marie Pédrot | |
| 2015-01-05 | Implementing a segment-viewer in CoqIDE. | Pierre-Marie Pédrot | |
| This allows a nifty display of the current state of the document through a dedicated progress bar. Also closes bug #3764. | |||
| 2014-12-17 | CoqIDE: cleanup jobs window on worker death | Enrico Tassi | |
| 2014-12-17 | CThread: use a different type for thread friendly in_channels | Enrico Tassi | |
| 2014-12-17 | CoqIDE: better messages | Enrico Tassi | |
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot | |
| Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads. | |||
| 2014-12-14 | Revert "Fixing bug #3817." | Pierre-Marie Pédrot | |
| This reverts commit ad2a0308b1592c7235714a2cca926f3b55accbb2. | |||
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | |
| 2014-12-07 | Protecting from a List.nth when applying a command, e.g. C-w, on no CoqIDE ↵ | Hugo Herbelin | |
| buffer. | |||
| 2014-12-07 | Ensuring that ide_slave and stm receive only .v files from CoqIDE. | Hugo Herbelin | |
| In particular, renouncing to original support for existing non .v files in CoqIDE (hoping it is ok for anyone). Please amend if better to propose. | |||
| 2014-12-01 | Remove dead code | Enrico Tassi | |
| 2014-11-27 | Feedback: API cleaned up, documented and made user extensible | Enrico Tassi | |
| 2014-11-24 | Fixing bug #3817. | Pierre-Marie Pédrot | |
| Coqtop was wrongly assuming that receiving a SIGINT when reading on a channel meant that the channel was closed, resulting in a crash when interrupting an idle coqtop from CoqIDE. To prevent this, we block SIGINTs when reading in ide_slave. | |||
| 2014-11-15 | Reworking the -color flag of coqtop. | Pierre-Marie Pédrot | |
| 2014-11-06 | Fixing compilation (name of module Richprinter) I partially feel | Hugo Herbelin | |
| responsible about. | |||
| 2014-11-04 | ide/Xmlprotocol: Cosmetics. | Yann Régis-Gianas | |
| 2014-11-04 | ide/Ide_slave.annotate: Implement annotate. | Regis-Gianas | |
| 2014-11-04 | ide/{ide_slave.ml, interfaces}: Coerce input and output of requests between ↵ | Regis-Gianas | |
| internal and external datatypes. | |||
| 2014-11-04 | ide/wg_ProofView: Do not refer to the {Proof} internal module, use ↵ | Regis-Gianas | |
| {Interface} instead. | |||
| 2014-11-04 | ide/{Xmlprotocol,Interface,Ide_slave}: New command "annotate". | Regis-Gianas | |
| - Extend the protocol with a new command called "annotate". - By the way, relax the dependencies between the "ide" package and the internal packages of Coq by *not* referring to external type definitions inside Interface. Indeed, the purpose of the protocol is to act as a barrier between the source tree of Coq and the source tree of Coqide. We should enforce this property. (Maybe one day coqide will be extracted from the source tree of Coq to live its own life.) | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |