diff options
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" [] |