New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

bug(tactic): Unexpected horizontal rule (thematic break) in parsed Markdown #277

Open

joneugster opened this issue Jan 26, 2025 · 0 comments

joneugster commented Jan 26, 2025

Verso fails to parse a tactic docstring which contains a horizontal rule. Consider the tactic

/--
This is a Horizontal rule:
***
it does not parse.
-/
syntax (name := MyNamespace.bad_tactic) "bad_tactic " : tactic

then adding a tactic block to the file

:::tactic MyNamespace.bad_tactic show:="bad_tactic"
:::

fails with Unexpected horizontal rule (thematic break) in parsed Markdown.

Would be nice if either support for such HR could be added or if the markdown parser would simply remove them (instead of crashing).

The text was updated successfully, but these errors were encountered:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment