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.

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

Preserve Markdown as-is when outputting HTML #3137

Closed
vlopezj opened this Issue Jun 18, 2018 · 3 comments

Comments

Projects
None yet
4 participants
@vlopezj
Contributor

vlopezj commented Jun 18, 2018

@ice1000 said on issue #2357 (comment):

Hi there, is it possible to compile the agda code blocks to html only and leave other parts of the markdown document unchanged?

When I'm compiling my lagda.md files to html, the ordinary text parts are made "Comments", preventing the markdown renderer to render it.

I think this would be a useful feature. I don't know if someone else will be interested in implementing it; but you are welcome to give it a try yourself.

To avoid changing existing behaviour, I would suggest an extra flag --preserve-comments, which would tell Agda to leave all non-Agda text as-is when outputting HTML. This flag would be valid for both the --html and the --latex output modes.

For the --latex mode, preserving comments is the current default behaviour. For completeness, we could also have a --no-preserve-comments flag.

For extra functionality, one could have the default behaviour for each mode (preserve comments or not) depend on the extension of the file.

It was @ak3n who originally implemented Markdown support… Perhaps he has some ideas or even a work-around for your use case.

@ice1000

This comment has been minimized.

Member

ice1000 commented Oct 24, 2018

Created a PR that might fix this.

@ice1000

This comment has been minimized.

Member

ice1000 commented Oct 26, 2018

For those who don't have patience to read the PR:

  • This should only work with the HTML backend:
    • It has something to do with the HTML header/footer
    • It's pointless to generate LaTeX/GHC/JS with comments not preserved
  • This will prevent the HTML renderer from escaping the non-Agda-code characters, so markdown symbols like > will be preserved as-is
  • This will remove the HTML header/footer in the generated file.
@asr

This comment has been minimized.

Member

asr commented Oct 30, 2018

@vlopezj, please add the 2.6.0 milestone.

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