Skip to content
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

agda highlight #69

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

agda highlight #69

wants to merge 1 commit into from

Conversation

lwoo1999
Copy link

screenshot_20190128_133832

@weisi
Copy link

weisi commented Jun 28, 2019

Is this PR still active?

@arcticicestudio
Copy link
Contributor

arcticicestudio commented Jun 28, 2019

@weisi The PR is still in the backlog, but requires a more detailed review and revision since I'm not familiar with Agda and the screenshot shows some elements that need to be changed regarding the coloring. As soon as the data transition of all Nord port projects to the new shiny website is completed there is more time again to process all the open issues and PRs from all Nord repositories.

@harryaskham
Copy link

Can confirm that as of today, patching this block into nord-theme.el works just fine. Not an advanced user so can't speak to the ergonomics of some of the color choices, but it's certainly a huge improvement over the default colorings one gets in Agda mode using default nord.

For now I've forked 0.5 as nord-agda-theme.el with (deftheme nord-agda ...).

If I get the time (and after learning more Agda...) I'll try to figure out where the theme diverges from guidelines, make the edits, and hopefully we can get this into main.

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

Successfully merging this pull request may close these issues.

4 participants