aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
* 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.
| * | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier.
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\|
| * Fix regression in Coqide's "forward one command" commandGravatar Xavier Leroy2016-08-14
| | | | | | | | | | | | | | | | In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".". In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase. The insertion point is moved only if it falls behind the phrase being executed. I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior. This commit restores the 8.4 behavior of "forward one command".
* | Adding a flag in CoqIDE to configure UNIX/Windows line ending.Gravatar Pierre-Marie Pédrot2016-07-26
| | | | | | | | Fixes both bugs #4924 and #4437.
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | | | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\|
* | Merge remote-tracking branch 'github/pr/223' into feedback-locationsGravatar Maxime Dénès2016-06-27
|\ \ | | | | | | | | | Was PR#223: Allow feedback messages to carry a location.
* | | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| | | | | | | | | | | | Cf CHANGES for details.
| | * Fix bug #4698: CoqIDE error dialogs piling up when coqtop dies.Gravatar Pierre-Marie Pédrot2016-06-27
| | | | | | | | | | | | | | | | | | Instead of relaunching the coqtop process and then open the warning window, we rather fire the warning and wait for the user to press the OK button before doing anything.
| * | [xmlproto] Remove duplicated deserialization.Gravatar Emilio Jesus Gallego Arias2016-06-25
| | |
| * | [feedback] Remove `ErrorMsg` in favor of `Message Error`.Gravatar Emilio Jesus Gallego Arias2016-06-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The ErrorMsg datatype was introduced to allow locations in messages, however, it was redundant with error and used only in one place. We remove it in favor of a more uniform treatment of messages with location. This patch also removes the use of `Loc.ghost` in one place. Lightly tested.
| * | [feedback] Allow messages to carry a location.Gravatar Emilio Jesus Gallego Arias2016-06-25
| | | | | | | | | | | | | | | | | | | | | The new warnings mechanism may which to forward a location to IDEs. This also makes sense for other message types. Next step is to remove redundant MsgError feedback type.
| * | [feedback] Add optional ?loc parameter to loggers.Gravatar Emilio Jesus Gallego Arias2016-06-25
| | | | | | | | | | | | | | | | | | | | | | | | This is a first step to relay location info in an uniform way, as needed by warnings and other mechanisms. The location info remains unused for now, but coqtop printing could take advantage of it if so wished.
| * | [feedback] Remove unused tag on `Debug` level.Gravatar Emilio Jesus Gallego Arias2016-06-25
|/ / | | | | | | IMO level indicators are not the proper place to store this information.
* | ideslave: do not bail out in case of XML errorGravatar Enrico Tassi2016-06-16
| | | | | | | | | | Used to be an `exit 1`, now an error message is printed on stderr. This helps people experimenting with the XML protocol.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 10:49:49 +0000