aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
...
| * Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
|\ \
* \ \ Merge PR#355: Remove unused feedback_content: GoalsGravatar Maxime Dénès2017-01-30
|\ \ \
| | * | Fix documentation typos.Gravatar Guillaume Melquiond2017-01-27
| | | |
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\ \ \ \ | | |/ / | |/| |
| * | | Fix broken .aux machinery.Gravatar Guillaume Melquiond2017-01-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Coq expects aux_file_name_for to give the aux file corresponding to the input file whichever its Coq-related extension, be it .v or .vo or .vio. Commit 3e6fa1c broke this contract when fixing bug #5183. As a consequence, depending on the execution path, Coq would try to save or load from either .foo.aux or .foo.vo.aux or .foo.vio.aux. This commit reverts 3e6fa1c and fixes bug #5183 much earlier in the call chain by not initializing hints when the input file does not end with .v. This also restores 8.5 behavior with respect to aux file naming.
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\| | |
| * | | [merlin] Adjust merlin for ide.Gravatar Emilio Jesus Gallego Arias2016-11-30
| | | |
| * | | Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
| | | |
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\| | | | |_|/ |/| |
| * | Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341. It turns out that calling from fake_ide the STM commands that were removed by this PR requires an extension of the XML protocol. So postponing the integration.
| * | [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | I think these commands never make a lot of sense on scripts other than debugging and we have better methods now. The last remaining command, used for the tty emulation has been renamed to VtBack, but it should go away at some point too once the legacy interfaces are removed.
| * | Coqide: fixing default local links for refman and stdlib.Gravatar Hugo Herbelin2016-11-11
| | |
| * | Making explicit that a result is discarded (ocaml warning).Gravatar Hugo Herbelin2016-11-11
| | |
| | * Remove unused feedback_content: GoalsGravatar CJ Bell2016-11-10
| |/ |/|
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\ \
| | * Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Gravatar Guillaume Melquiond2016-10-01
| |/ | | | | | | | | | | | | | | | | | | For now, the only meaningful user is "Set Warnings". Example: Section Bar. Local Set Warnings Append "-foo". (* warning foo is now disabled *) End Bar. (* foo is now reenabled, assuming it was before entering the section *)
| * Merge branch 'v8.5' into v8.6Gravatar Maxime Dénès2016-09-30
| |\
| * | Fix bug #4798: compat notations should not modify the parser.Gravatar Pierre-Marie Pédrot2016-09-29
| | | | | | | | | | | | | | | | | | This is a quick fix. The Metasyntax module should be thoroughly revised in trunk, because it starts featuring a lot of spaghetti code and redundant data.
| * | Do not stop propagation of signals when Coq is busy (bug #3941).Gravatar Guillaume Melquiond2016-09-28
| | | | | | | | | | | | | | | | | | | | | | | | When inserting a character in an already processed buffer, a message is sent to Coq so that the proof is backtracked and the character is inserted. If a second character is inserted while Coq is still busy with the first message, the action is canceled, but the signal is no longer dropped so that the second character is properly inserted.
| | * Make error message more helpful.Gravatar Théo Zimmermann2016-09-28
| | | | | | | | | CoqIDE does not have a "display" menu. It has a "view" menu with a list of display options.
| * | Fix bug #4553: CoqIDE gives warnings about deprecated GTK features.Gravatar Pierre-Marie Pédrot2016-09-27
| | |
* | | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | I hadn't realized that this PR uses OCaml's 4.03 inlined records feature. I will advocate again for a switch to the latest OCaml stable version, but meanwhile, let's revert. Sorry for the noise. This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
* | | Merge remote-tracking branch 'github/pr/283' into trunkGravatar Maxime Dénès2016-09-22
|\ \ \ | | | | | | | | | | | | Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
* | | | Removing dead code in CoqIDE.Gravatar Pierre-Marie Pédrot2016-09-21
| | | | | | | | | | | | | | | | | | | | There was a pile of dead code inherited from Cameleon just sitting around and not used at all. This code was introduced in 2003 and never actually used.
| * | | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We get rid of tuples containing booleans (typically for universe polymorphism) by replacing them with records. The previously common idom: if pi2 kind (* polymorphic *) then ... else ... becomes: if kind.polymorphic then ... else ... To make the construction and destruction of these records lightweight, the labels of boolean arguments for universe polymorphism are now usually also called "polymorphic".
* | | Make the Coq codebase independent from Ltac-related code.Gravatar Pierre-Marie Pédrot2016-09-16
|\ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We untangle many dependencies on Ltac datastructures and modules from the lower strata, resulting in a self-contained ltac/ folder. While not a plugin yet, the change is now very easy to perform. The main API changes have been documented in the dev/doc/changes file. The patches are quite rough, and it may be the case that some parts of the code can migrate back from ltac/ to a core folder. This should be decided on a case-by-case basis, according to a more long-term consideration of what is exactly Ltac-dependent and whatnot.
* \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\ \ \ \ | | |/ / | |/| |
| * | | CoqIDE: push to message win feedback Message(Debug,Info,Notice)Gravatar Enrico Tassi2016-09-13
| | | |
| | * | Removing the last uses of Pptactic in the lower layers.Gravatar Pierre-Marie Pédrot2016-09-09
| | | |
| | * | Making Vernacexpr independent from Tacexpr.Gravatar Pierre-Marie Pédrot2016-09-08
| |/ / |/| |
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \
* \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-07
|\ \ \ \ | | |/ / | |/| |
| * | | CoqIDE: Errors are sticky (fix #4368)Gravatar Enrico Tassi2016-09-07
| | | |
| * | | coqide: use Document instead of tags to detect sentences to `Skip (#4829)Gravatar Enrico Tassi2016-09-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When one jumps from a focused area to a point after the focused zone, sentences that are already processed (in the Doc.context of the focused area) have not to be processed again (they are tagged as `Skip). Detection of such sentences was based on tags (i.e. colors) that is shaky. Now we use the sentence-marks as stored in the document data structure.
| * | | xml_printer: use sensible names for putc and putsGravatar Enrico Tassi2016-09-05
| | | | | | | | | | | | | | | | They used to be called output and output' ...
| * | | feedback: support multiple feedback listenersGravatar Enrico Tassi2016-09-05
| | | | | | | | | | | | | | | | So that a module can add his own and look at the traffic
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\| | |
| * | | Fix bug #5051: Large outputs are garbled.Gravatar Pierre-Marie Pédrot2016-08-30
| | | | | | | | | | | | | | | | | | | | Instead of relying on the current position of the cursor, we rather use a dedicated mark in the message view.
* | | | CLEANUP: removing a function that duplicates its counterpart already present ↵Gravatar Matej Kosik2016-08-30
| | | | | | | | | | | | | | | | in the Ocaml standard library
| * | | Fix bug #4421: Messages dialog in Coqide resets.Gravatar Pierre-Marie Pédrot2016-08-29
| | | |
| * | | CoqIDE preserves unknown preferences.Gravatar Pierre-Marie Pédrot2016-08-29
| | | | | | | | | | | | | | | | | | | | This allows a smoother transition between various versions of CoqIDE, by not erasing options which are unknown at the present time.
| * | | Fix inefficiency in CoqIDE display of tagged text.Gravatar Pierre-Marie Pédrot2016-08-29
| | | | | | | | | | | | | | | | | | | | The helper code in LablGTK is algorithmically slow, so that we rather reimplement it as a small helper function.
* | | | CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Gravatar Matej Kosik2016-08-26
| | | |
* | | | CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeGravatar Matej Kosik2016-08-25
| | | |
* | | | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
|/ / /
| * | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | Suggested by @ppedrot
| * | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | | | | | | | | | | As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 20:09:31 +0000