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

Import dark theme from https://github.com/dennis84/codemirror-themes/… #1132

Closed
wants to merge 1 commit into from

Conversation

peepeetee
Copy link

…blob/main/theme/github-dark.ts

Import dark theme from https://github.com/dennis84/codemirror-themes/blob/main/theme/github-dark.ts

The correct solution here is to go back to https://discuss.codemirror.net/t/dynamic-light-mode-dark-mode-how/4709/5 and look at the solution: https://discuss.codemirror.net/t/dynamic-light-mode-dark-mode-how/4709/2

The idea is to use the default theme implementation and not use the compatibility bodge. This would probably involve including some theme files in the source, and I would prefer a theme picker as shown https://codemirror.net/5/demo/theme.html ( this is codemirror5 but you get the idea)

@inducer
Copy link
Owner

inducer commented Oct 17, 2024

Thanks! And d'oh! Just last night I also pushed a fix for #1084, in b3d1181. Would you still prefer the Github theme? I'd be happy to bring it in if you think it's a net win.

I thought about a theme picker. (Probably we'd need two: one for dark and one for light.) That's a slightly bigger change, but manageable. If you'd like it, file an issue?

@peepeetee peepeetee marked this pull request as draft October 18, 2024 01:11
@peepeetee
Copy link
Author

Thanks! And d'oh! Just last night I also pushed a fix for #1084, in b3d1181. Would you still prefer the Github theme? I'd be happy to bring it in if you think it's a net win.

I thought about a theme picker. (Probably we'd need two: one for dark and one for light.) That's a slightly bigger change, but manageable. If you'd like it, file an issue?

Yee, I had to delete my browser cache but I can confirm that it is working now.

I have converted this pr to a draft, not sure how to convert it to an issue. I could close it and open a new issue if you want

@inducer
Copy link
Owner

inducer commented Oct 18, 2024

New issue sounds good if what you'd like to request is unrelated to this PR.

@peepeetee peepeetee closed this Oct 18, 2024
@peepeetee
Copy link
Author

New issue sounds good if what you'd like to request is unrelated to this PR.

#1134

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

Successfully merging this pull request may close these issues.

2 participants