Render issue using `<details>` blocks

[fredrik-bakke]

Hi! I recently filed this bug with GitHub, and they referred me here, so I will just copy parts of that ticket below.

Literate Agda markdown files with <details> tags are not displayed properly in the web interface in certain instances.

Reproduction Steps

Push a .lagda.md file to your repository containing code of the following form

<details>
```agda
open import Agda.Primitive

Some text.

Then view it in the GitHub web interface. The code will not be displayed properly, and "Some text." will be hidden as part of the details.

This seems to be an issue with the empty line in the Agda code block. If there are no blank lines in this block, only the correct contents are hidden.

For an example of the display issue, please have a look at the following link. All of the file's contents are hidden although they should not be, and some code is displayed improperly.
<https://github.com/fredrik-bakke/agda-unimath/blob/master/src/foundation/univalence.lagda.md>

In their reply, they also noted the following

Thanks for reaching out to GitHub Support about problem when using the <details> tag. I do see this problem when there is a blank line included in a code block inside of a <details> block. I did also find that you can reproduce this by including a blank line inside the <details> block that is outside of the code block.

Lastly, I noted in a reply to them that there is a second issue with <details> blocks. Namely as follows.

I realize now that there are two aspects to this bug. The first, as previously mentioned, is that if there are blank lines inside the <details> block, it hides contents after the block ends. The other issue is that even when there are no blank lines inside the block, it does not display some elements correctly. For instance, with the following code

<details>
```agda
open import Agda.Primitive

The contents of the `<details>` block is displayed as

agda open import Agda.Primitive

With the escape characters (`) visible, without the code highlighting, and with the newlines changed to spaces.

Best Fredrik Bakke

[wooorm]

If you want to mix markdown and HTML, use blank lines:

<details>

code

</details>

->

``` code ```

For more info, see the existing (closed) issues, e.g., such as with this search

[fredrik-bakke]

Oh. Well, thanks for the help!