aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Collapse)Author
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.
2015-06-16Fix by Enrico on CoqIDE not locating errors anymore since 550da87456a.Hugo Herbelin
2015-06-07Fixing bug #4233: The command Restart is not fontified correctly.Pierre-Marie Pédrot
2015-05-29coqide: don't require ocaml >= 4Enrico Tassi
2015-05-26Jump to error line in CoqIDE grabs focus of the textview.Pierre-Marie Pédrot
2015-05-25CoqIDE columns in error and job panels can be sorted.Pierre-Marie Pédrot
This grants wish #4194.
2015-05-05Compatibility ocaml 3.12.Hugo Herbelin
2015-05-05Granting wish #4221.Pierre-Marie Pédrot
2015-04-27Improve syntax highlighting.Guillaume Melquiond
- Arithmetic operators and brackets are no longer recognized as bullets, unless they follow a stop or start a line. - Most vernacular commands are no longer highlighted when used inside proof scripts. - Coqdoc comments now take precedence over regular comments.
2015-04-26Open the file chooser even if there is no current session. (Fix bug #4206)Guillaume Melquiond