aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Collapse)Author
2016-01-02Remove some unused functions.Guillaume Melquiond
Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot.
2016-01-02Remove some useless type declarations.Guillaume Melquiond
2016-01-02Avoid warnings about loop indices.Guillaume Melquiond
2016-01-02Remove useless rec flags.Guillaume Melquiond
2016-01-01Fix typos.Guillaume Melquiond
2016-01-01Remove unplugged button from the interface.Guillaume Melquiond
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-14Fixing little bug of coq_makefile with unterminated comment.Hugo Herbelin
Force failing when reaching end of file with unterminated comment when parsing Make (project) file.
2015-12-14CoqIDE: add 'you need to restart CoqIDE after changing shortcuts' messageEnrico Tassi
2015-12-14Revert PMP's fix of #2498, which introduces an incompatibility with lablgtkMaxime Dénès
2.14. Debian ships with lablgtk 2.16 only since a few months, so we apply the fix to trunk instead. This reverts commits: 490160d25d3caac1d2ea5beebbbebc959b1b3832. ef8718a7fd3bcd960d954093d8c636525e6cc492. 6f9cc3aca5bb0e5684268a7283796a9272ed5f9d. 901a9b29adf507370732aeafbfea6718c1842f1b.
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-30Fix typo.Guillaume Melquiond
2015-10-22Using GADTs in Xmlprotocol.Pierre-Marie Pédrot
This removes 109 Obj.magic in one patch!
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-08Goptions: new value type: optional stringEnrico Tassi
These options can be set to a string value, but also unset. Internal data is of type string option.
2015-09-26Use default GTK styles for CoqIDE tags.Pierre-Marie Pédrot
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-24Fixing unsetting of CoqIDE tags.Pierre-Marie Pédrot
2015-09-21Change the default modifiers for navigation. (Fix bug #4295)Guillaume Melquiond
On most systems (including Windows, according to the bug report), shortcuts Ctrl+Alt+Arrows are preempted by the window manager by default. So don't use them for navigation in Coqide by default. Note that this change only has an impact when installing on a fresh system; it won't change anything for existing users.
2015-09-20Rich printing of CoqIDE protocol failure.Pierre-Marie Pédrot
2015-09-20Rich printing of messages.Pierre-Marie Pédrot
2015-09-20Rich printing of goals.Pierre-Marie Pédrot
2015-09-20Adding rich printing primitives.Pierre-Marie Pédrot
2015-09-20Do not canonicalize messages received by CoqIDE.Pierre-Marie Pédrot
2015-09-20Pluging in tag preferences into buffer printing.Pierre-Marie Pédrot
2015-09-20Adding standard printing tags to CoqIDE.Pierre-Marie Pédrot
2015-09-20Adding a tag preferencePierre-Marie Pédrot
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-15Removing a warning in CoqOps.Pierre-Marie Pédrot
2015-09-13Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-12Fixing bug #2498: Coqide navigation preferences delayed effect.Pierre-Marie Pédrot
2015-09-10Extending the grammar for CoqIDE preferences so as to match trunk.Pierre-Marie Pédrot
2015-08-31Switching to an event-based mechanism for CoqIDE preferences.Pierre-Marie Pédrot
There is no remaining hook in the preferences. In particular, the refresh_editor_hook is gone.
2015-08-26Replacing old-style preferences in CoqIDE.Pierre-Marie Pédrot
There is no remaining global preference record anymore, every preference is now defined in the new event-based style.
2015-08-22Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-17Highlighting of the "Next Obligation" command in CoqIDE.Pierre-Marie Pédrot
2015-08-16Using the new preference mechanism for colors in CoqIDE.Pierre-Marie Pédrot
A lot of legacy code has been removed in the process in favour of signal-based interactions.
2015-08-16Taking advantage of the new type of preferences.Pierre-Marie Pédrot
We use uniform functions instead of code duplication. Likewise, we disentangle the hook mechanisms by using callbacks connected to preferences instead. Only the easy hook bits were removed. The most awing one, the editor refreshing hook, is still alive.
2015-08-16Turning CoqIDE preferences into new style.Pierre-Marie Pédrot
Some old style references remain because all type converters are not implemented yet.
2015-08-16Simplifying CoqIDE preferences mechanism.Pierre-Marie Pédrot
We use a class-based system instead of the old record-based system. This allows for more uniformity and the possibility to define complex interactions with preferences based on GTK signals. This will allow to simplify some architectural choices.
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
2015-08-02Failing when reaching end of file with unterminated comment whenHugo Herbelin
parsing Make (project) file.
2015-07-28Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)Guillaume Melquiond
File system.ml seemed like a better choice than util.ml for sharing the code, but it was bringing a bunch of useless dependencies to the IDE. There are presumably several other tools that would benefit from using open_utf8_file_in instead of open_in, e.g. coqdoc.
2015-07-11CoqIDE: recenter on backtrack (Close: #4277)Enrico Tassi
2015-07-10Highlighting Universe in CoqIDE.Hugo Herbelin
2015-07-08Ide: fix bug #4284 for goodMatthieu Sozeau
Correct folding order over the named_list_context.
2015-07-08Bug 4284: Tentative bugfix for detyping exception.Matthieu Sozeau
2015-06-19Make end-of-proof output consistent across toplevels.Guillaume Melquiond
Ideally, the code should be shared between the various toplevels, but this is a lot more work than just fixing a few strings.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-24 12:56:32 +0000