on master help sign in
Merge pull request #4041 from idris-lang/revert-4021-fix-dump-highlights

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

commitdb95c2b5339a317e72466f1b9cdc098328a415af authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateFri 1 Sep 2017, 11:25 (9 years ago) parent5aa99ef054978c
1 file changed+3−4
src/Idris/Output.hs+3−4
src/Idris/Output.hs+3−4
@@ -234,15 +234,14 @@ sendParserHighlighting =
234234
235235sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()
236236sendHighlighting highlights =
237− do let highlights_uniq = nub highlights
238− ist <- getIState
237+ do ist <- getIState
239238 case idris_outputmode ist of
240239 RawOutput _ -> updateIState $
241240 \ist -> ist { idris_highlightedRegions =
242− highlights_uniq ++ idris_highlightedRegions ist }
241+ highlights ++ idris_highlightedRegions ist }
243242 IdeMode n h ->
244243 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)
245− | (fc, annot) <- highlights_uniq, fullFC fc
244+ | (fc, annot) <- highlights, fullFC fc
246245 ]
247246 in case fancier of
248247 [] -> return ()