Markdown→HTML pipeline mishandles empty code blocks

[ncfavier]

Markdown→HTML pipeline mishandles empty code blocks

[ncfavier]

tokenStream produces a single token for the whole empty code block:

(1,"```agda\n```\n",Aspects {aspect = Just Markup, otherAspects = fromList [], note = "", definitionSite = Nothing, tokenBased = TokenBased})

but then code splits on these Markup tokens and treats the result as alternating code and markup, which is wrong in this case.

I think the right thing to do here would be to split Markup into MarkupStart and MarkupEnd.

[andreasabel]

tokenStream is

agda/src/full/Agda/Interaction/Highlighting/HTML/Base.hs

Lines 283 to 293 in 82f3427

	tokenStream
	:: Text -- ^ The contents of the module.
	-> HighlightingInfo -- ^ Highlighting information.
	-> [TokenInfo]
	tokenStream contents info =
	map (\ ((mi, (pos, c)) :| xs) ->
	(pos, c :| map (snd . snd) xs, fromMaybe mempty mi)) $
	List1.groupBy ((==) `on` fst) $
	zipWith (\pos c -> (IntMap.lookup pos infoMap, (pos, c))) [1..] (T.unpack contents)
	where
	infoMap = toMap info

code is

agda/src/full/Agda/Interaction/Highlighting/HTML/Base.hs

Line 307 in 82f3427

MdFileType -> map mkMd . chunksOf 2 . splitByMarkup

[andreasabel]

I think the right thing to do here would be to split Markup into MarkupStart and MarkupEnd.

@ncfavier , thanks for this analysis!
I am not familiar with the code, could you submit a PR implementing this idea?

[ncfavier]

I think the right thing to do here would be to split Markup into MarkupStart and MarkupEnd.

That turned out not to be necessary: #6880