diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-16 03:57:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-16 04:52:08 +0200 |
| commit | cda147bf2b22e5230abd6fb604e9b8c105828717 (patch) | |
| tree | 88ab3ce142b9e7a214edfb348cdc28052d6299cd /ide/wg_MessageView.ml | |
| parent | 5a90c69f8e4699f205ec3e59cfd49ad9fb9f6f87 (diff) | |
Taking advantage of the new type of preferences.
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.
Diffstat (limited to 'ide/wg_MessageView.ml')
0 files changed, 0 insertions, 0 deletions