aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
* Hardcode how coqide have to look for coqtop in MacOS bundleGravatar Pierre Boutillier2015-02-13
| | | | Sorry, that is ugly. Please revert if you see a better way to do it.
* Selection of the current word in CoqIDE looks at all buffers.Gravatar Pierre-Marie Pédrot2015-02-13
|
* Trying to fix bug #3930.Gravatar Pierre-Marie Pédrot2015-02-13
| | | | | | 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.
* Tentative fix for CoqIDE randomly dropping deletions.Gravatar Pierre-Marie Pédrot2015-02-12
| | | | | | 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.
* Fixing bug #3261.Gravatar Pierre-Marie Pédrot2015-02-12
|
* Focussing on message view in CoqIDE when a message is pushed.Gravatar Pierre-Marie Pédrot2015-02-12
| | | | Also fixes bug #4030.
* Fixing bug #4023.Gravatar Pierre-Marie Pédrot2015-02-12
|
* Reinstauring backtrace display in CoqIDE.Gravatar Pierre-Marie Pédrot2015-02-11
|
* Making undo/redo atomic in CoqIDE.Gravatar Pierre-Marie Pédrot2015-02-10
|
* More efficient Richpp.Gravatar Pierre-Marie Pédrot2015-02-06
| | | | We build the rich XML at once without generating the printed string.
* Fixing bug #3996.Gravatar Pierre-Marie Pédrot2015-02-04
|
* Made the CoqIDE progress gutter clickable.Gravatar Pierre-Marie Pédrot2015-01-29
|
* Made replacing of text in CoqIDE atomic w.r.t. the undo/redo.Gravatar Pierre-Marie Pédrot2015-01-25
|
* Fixing bug #3947.Gravatar Pierre-Marie Pédrot2015-01-25
|
* CoqIDE: a Make file to build coqidetop toploopGravatar Enrico Tassi2015-01-14
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Removing GUtil dependency from ide/document.ml.Gravatar Pierre-Marie Pédrot2015-01-05
| | | | We reimplement a quick-n-dirty Gtk-free signal handler.
* Adding an option to deactivate the progress bar.Gravatar Pierre-Marie Pédrot2015-01-05
|
* Implementing a segment-viewer in CoqIDE.Gravatar Pierre-Marie Pédrot2015-01-05
| | | | | | | This allows a nifty display of the current state of the document through a dedicated progress bar. Also closes bug #3764.
* CoqIDE: cleanup jobs window on worker deathGravatar Enrico Tassi2014-12-17
|
* CThread: use a different type for thread friendly in_channelsGravatar Enrico Tassi2014-12-17
|
* CoqIDE: better messagesGravatar Enrico Tassi2014-12-17
|
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | | | | | | | | | | | 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.
* Revert "Fixing bug #3817."Gravatar Pierre-Marie Pédrot2014-12-14
| | | | This reverts commit ad2a0308b1592c7235714a2cca926f3b55accbb2.
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* Protecting from a List.nth when applying a command, e.g. C-w, on no CoqIDE ↵Gravatar Hugo Herbelin2014-12-07
| | | | buffer.
* Ensuring that ide_slave and stm receive only .v files from CoqIDE.Gravatar Hugo Herbelin2014-12-07
| | | | | | 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.
* Remove dead codeGravatar Enrico Tassi2014-12-01
|
* Feedback: API cleaned up, documented and made user extensibleGravatar Enrico Tassi2014-11-27
|
* Fixing bug #3817.Gravatar Pierre-Marie Pédrot2014-11-24
| | | | | | | | 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.
* Reworking the -color flag of coqtop.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Fixing compilation (name of module Richprinter) I partially feelGravatar Hugo Herbelin2014-11-06
| | | | responsible about.
* ide/Xmlprotocol: Cosmetics.Gravatar Yann Régis-Gianas2014-11-04
|
* ide/Ide_slave.annotate: Implement annotate.Gravatar Regis-Gianas2014-11-04
|
* ide/{ide_slave.ml, interfaces}: Coerce input and output of requests between ↵Gravatar Regis-Gianas2014-11-04
| | | | internal and external datatypes.
* ide/wg_ProofView: Do not refer to the {Proof} internal module, use ↵Gravatar Regis-Gianas2014-11-04
| | | | {Interface} instead.
* ide/{Xmlprotocol,Interface,Ide_slave}: New command "annotate".Gravatar Regis-Gianas2014-11-04
| | | | | | | | | | | | | | - 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.)
* Install index_urls.txt in a location where coqide might actually find it.Gravatar Guillaume Melquiond2014-10-24
|
* Fixing order of hypothesis in goal hypotheses compaction for coqtop.Gravatar Hugo Herbelin2014-10-24
|
* fix parsing of ---- +++++ ***** in CoqIDEGravatar Enrico Tassi2014-10-23
|
* Pushing Pierre's factorization of names in goal context printing fromGravatar Hugo Herbelin2014-10-22
| | | | | | coqide to coqtop. (Joint work with Pierre)
* CoqIDE: fix parsing of multicharacter bulletsGravatar Enrico Tassi2014-10-22
|
* Fix the way lexeme start is computed (Close 3737)Gravatar Enrico Tassi2014-10-22
|
* STM: report the (structured) goals as XMLGravatar Carst Tankink2014-10-01
| | | | | The leafs of the XML trees are still pretty-printed strings, but this could be refined later on.
* Factored out IDE goal structure.Gravatar Carst Tankink2014-10-01
| | | | | | | | | | | | 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.
* CoqIDE: new message to print ASTGravatar Enrico Tassi2014-09-29
|
* Remove pointless regex for '""' as the empty string already matches it.Gravatar Guillaume Melquiond2014-09-17
|
* Fix highlighting of "Hint Unfold" and "Hint Rewrite".Gravatar Guillaume Melquiond2014-09-17
|
* Properly highlight the Export keyword.Gravatar Guillaume Melquiond2014-09-17
|
* Fix ambiguous regex in syntax highlighting.Gravatar Guillaume Melquiond2014-09-17
| | | | | | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 02:51:50 +0000