| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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.) | |||
| 2014-10-24 | Install index_urls.txt in a location where coqide might actually find it. | Guillaume Melquiond | |
| 2014-10-24 | Fixing order of hypothesis in goal hypotheses compaction for coqtop. | Hugo Herbelin | |
| 2014-10-23 | fix parsing of ---- +++++ ***** in CoqIDE | Enrico Tassi | |
| 2014-10-22 | Pushing Pierre's factorization of names in goal context printing from | Hugo Herbelin | |
| coqide to coqtop. (Joint work with Pierre) | |||
| 2014-10-22 | CoqIDE: fix parsing of multicharacter bullets | Enrico Tassi | |
| 2014-10-22 | Fix the way lexeme start is computed (Close 3737) | Enrico Tassi | |
| 2014-10-01 | STM: report the (structured) goals as XML | Carst Tankink | |
| The leafs of the XML trees are still pretty-printed strings, but this could be refined later on. | |||
| 2014-10-01 | Factored out IDE goal structure. | Carst Tankink | |
| The more structured goal record type of CoqIDE is also useful for other interfaces (in particular, for PIDE). To support this, the datatype was factored out to the Proof module. In addition, the record gains a type parameter, to allow interfaces to adapt the output to their needs. To accommodate this type, the Proof module also gains the map_structured_proof that takes a Proof.proof and a function on the individual goals (in the context of an evar map) and produces a structured goal based on the goal transformer. | |||
| 2014-09-29 | CoqIDE: new message to print AST | Enrico Tassi | |
| 2014-09-17 | Remove pointless regex for '""' as the empty string already matches it. | Guillaume Melquiond | |
| 2014-09-17 | Fix highlighting of "Hint Unfold" and "Hint Rewrite". | Guillaume Melquiond | |
| 2014-09-17 | Properly highlight the Export keyword. | Guillaume Melquiond | |
| 2014-09-17 | Fix ambiguous regex in syntax highlighting. | Guillaume Melquiond | |
| This fix considerably speeds up syntax highlighting. It also avoids burning 100% CPU when typing long identifiers. Finally, identifiers longer than 20 characters are now properly highlighted, since the stack of the automaton no longer overflows because of them. | |||
| 2014-09-17 | Fix broken syntax highlighting for Coq files using "Proof constr". | Guillaume Melquiond | |
| See Eqdep_dec.v for instance. Module declarations were not highlighted because the IDE wrongly believed they were used inside an unterminated proof. | |||
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin | |
| instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions. | |||
| 2014-09-09 | IDE: escape popup text (close: 3600) | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |