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

Add `--dump-highlight` cli flag to output highlighting information #3389

Open
ice1000 opened this Issue Nov 14, 2018 · 3 comments

Comments

Projects
None yet
4 participants
@ice1000
Member

ice1000 commented Nov 14, 2018

In some format like json, xml, etc. So we can create external renderers.
The HTML backend and Vim backend can be replaced by this entirely maybe.

Proposed by @dramforever, I like this idea.

@ice1000

This comment has been minimized.

Member

ice1000 commented Nov 14, 2018

He says Jekyll has nothing to do with Agda (#3386), so does HTML.

@dramforever

This comment has been minimized.

dramforever commented Nov 14, 2018

We discussed this in private a while ago, and I felt that dealing with technicalities like that is outside of the scope of the official Agda compiler.

It (Edit: I meant a hypothetical tool that deals with all kinds of formats) doesn't even need to be third-party -- it can even just reside within agda/agda. I just don't think it's worth cluttering the compiler.

@nad

This comment has been minimized.

Contributor

nad commented Nov 14, 2018

See also #3186.

@jespercockx jespercockx added this to the icebox milestone Nov 15, 2018

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