on master help sign in
Merge pull request #4021 from jfdm/fix-dump-highlights

Fix #4020: Fix duplication in output of `--hightlight`.

commit0b78de1701a846a712b9652b3853fce29a19895d authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateSat 26 Aug 2017, 08:56 (9 years ago) parente2843b0c51fd2d
1 file changed+4−3
src/Idris/Output.hs+4−3
src/Idris/Output.hs+4−3
@@ -234,14 +234,15 @@ sendParserHighlighting =
234234
235235sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()
236236sendHighlighting highlights =
237− do ist <- getIState
237+ do let highlights_uniq = nub highlights
238+ ist <- getIState
238239 case idris_outputmode ist of
239240 RawOutput _ -> updateIState $
240241 \ist -> ist { idris_highlightedRegions =
241− highlights ++ idris_highlightedRegions ist }
242+ highlights_uniq ++ idris_highlightedRegions ist }
242243 IdeMode n h ->
243244 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)
244− | (fc, annot) <- highlights, fullFC fc
245+ | (fc, annot) <- highlights_uniq, fullFC fc
245246 ]
246247 in case fancier of
247248 [] -> return ()