diff options
| author | Jim Fehrle | 2018-09-03 14:51:21 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-09-03 14:51:21 -0700 |
| commit | fa239fdca9fc07e65aec424c9a0c88128c43c329 (patch) | |
| tree | d62cd1a73782b34026ba8b2525137b15cf317166 /ide/ideutils.ml | |
| parent | 6f1c4ac389e595e09fdf4653847d8c3ccca0befb (diff) | |
Fix for issue #8378. If the string matches the regex, output the
part before the regex match with full highlights. (Duh)
Diffstat (limited to 'ide/ideutils.ml')
| -rw-r--r-- | ide/ideutils.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 960beb8455..03396a5a5c 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -71,15 +71,15 @@ let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = let rmark = `MARK (buf#create_mark buf#start_iter) in (* insert the string, but don't apply diff highlights to white space at the begin/end of line *) let rec insert_str tags s = + let etags = try List.hd !dtags :: tags with hd -> tags in try - let _ = Str.search_forward nl_white_regex s 0 in + let start = Str.search_forward nl_white_regex s 0 in + insert_with_tags buf mark rmark etags (String.sub s 0 start); insert_with_tags buf mark rmark tags (Str.matched_group 1 s); let mend = Str.match_end () in insert_str tags (String.sub s mend (String.length s - mend)) - with Not_found -> begin - let etags = try List.hd !dtags :: tags with hd -> tags in + with Not_found -> insert_with_tags buf mark rmark etags s - end in let rec insert tags = function | PCData s -> insert_str tags s |
