Fix handling of empty code blocks in HTML/MD backend

[ncfavier]

Instead of assuming the runs of tokens alternate between background and code, look at each run to determine what kind of tokens it contains, just like for org mode.

Fixes #6873

cc @ice1000 since you authored the original mkMd.

[ice1000]

Looks legit! Is there any chance where you'll be having highlighting in a background text?

[ncfavier]

A priori no, since the literate parsers can be seen to never output a Comment (Background) token adjacent to a Code token.

[ice1000]

CI fails

[ncfavier]

Yeah, I don't think it's due to this PR.

[andreasabel]

@Mergifyio rebase

[mergify]

rebase

✅ Branch has been successfully rebased

[andreasabel]

@wenkokke : Would you have the capacity now to test this PR on plfa?

[wenkokke]

Unfortunately, it seems PLFA doesn't compile with Agda 2.6.4, so it's difficult to test this PR:

~/plfa/src/plfa/part1/Lists.lagda.md:56,3-6
Set₁ is not less or equal than Set
when checking that the type Set of an argument to the constructor
[]′ fits in the sort Set of the datatype.
Note: this argument is forced by the indices of []′, so this
definition would be allowed under --large-indices.

[andreasabel]

@wenkokke : This version of lists is now only allowed with flag --large-indices:
https://github.com/plfa/plfa.github.io/blob/e11d7240e21af68670d3c0d7354a322d425b4308/src/plfa/part1/Lists.lagda.md?plain=1#L64-L66

data List′ : Set → Set where
  []′  : ∀ {A : Set} → List′ A
  _∷′_ : ∀ {A : Set} → A → List′ A → List′ A

agda/CHANGELOG.md

Lines 227 to 242 in 338efc9

	* [**Breaking**] Constructor arguments are no longer allowed to store
	values of a type larger than their own sort, even when these values
	are forced by the indices of a constructor.
	This fixes a particular instance of the incompatibility between
	structural recursion and impredicativity, which could previously be
	exploited through the use of large data-type indices.
	(see [#6654](https://github.com/agda/agda/issues/6654)).
	This behaviour can be controlled with the flag `--large-indices`. Note
	that, when `--large-indices` is enabled, forced constructor arguments
	should not be used for termination checking. The flag
	`--[no-]forced-argument-recursion` makes the termination checker skip
	these arguments entirely. When `--safe` is given, `--large-indices` is
	incompatible with `--without-K` _and_ incompatible with
	`--forced-argument-recursion`.

[wenkokke]

I believe this doesn't break PLFA.

[andreasabel]

Thanks, everyone!
I merged this in for the 2.6.4 release.