diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-22 21:59:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-22 22:32:46 +0200 |
| commit | d651d81a13d78f0466d2a08c06e7f2318c42da5f (patch) | |
| tree | c0b3d2f37232bd1613a6ef3c20fd3430a9cb6577 /ide | |
| parent | 0897d0f642c19419c513f9609782436bebf28f5b (diff) | |
An attempt to fix issue #5771 (error color hidden by warning color).
We change the relative priority of errors and warnings, so that the
error takes precedence.
It is unsure that it is universally the best choice. If the location
of the error is finer than the one of the warning, it is better. In
the other way round, it might be less good, e.g. if understanding the
warning helps to understand the error.
Maybe the best policy would be to test the relative locations of the
warning and error?
Trying to consider the error as more important, at the current time.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/tags.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/tags.ml b/ide/tags.ml index 08ca47a84..d389cde30 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -15,10 +15,11 @@ let make_tag (tt:GText.tag_table) ~name prop = module Script = struct + (* More recently defined tags have highest priority in case of overlapping *) let table = GText.tag_table () let comment = make_tag table ~name:"comment" [] - let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE] let warning = make_tag table ~name:"warning" [`UNDERLINE `SINGLE; `FOREGROUND "blue"] + let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE] let error_bg = make_tag table ~name:"error_bg" [] let to_process = make_tag table ~name:"to_process" [] let processed = make_tag table ~name:"processed" [] |