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

Highlight dyn as a keyword #224

Closed
vi opened this issue Oct 30, 2017 · 6 comments
Closed

Highlight dyn as a keyword #224

vi opened this issue Oct 30, 2017 · 6 comments
Labels
enhancement Something new the playground could do

Comments

@vi
Copy link

vi commented Oct 30, 2017

dyn is already implemented in nightly, so maybe dyn should be highlighted somehow in the playpen?

@shepmaster
Copy link
Member

shepmaster commented Oct 30, 2017

should be highlighted somehow

Syntax highlighting is provided by Ace — perhaps you'd be willing to submit a pull request to them?

in the playpen?

There is no playpen. There is only the playground.

@shepmaster shepmaster added enhancement Something new the playground could do help wanted Not immediately going to be prioritized — ask for mentoring instructions! labels Oct 30, 2017
@shepmaster shepmaster changed the title dyn should probably be already highlighted as a keyword. Highlight dyn as a keyword Oct 30, 2017
@vi
Copy link
Author

vi commented Oct 30, 2017

"Rust Playpen" =? "The Rust Playground" =? "play.rust-lang.org site".

@shepmaster
Copy link
Member

Sounds good, vim [sic]. Names have meanings and differences; the very old site was called the playpen.

@vi
Copy link
Author

vi commented Oct 30, 2017

Only now realized that there is a difference while trying to find a proof that they're the same.

@shepmaster
Copy link
Member

Thank you for opening an issue on Ace. Once there's a corresponding PR, I can probably hack up the existing Rust highlighter using the diff. I just don't want to be forced into maintaining a perpetual fork of an open source project without very good reason.

@vi
Copy link
Author

vi commented Oct 31, 2017

The PR has been merged.

shepmaster added a commit that referenced this issue Nov 1, 2017
@shepmaster shepmaster removed the help wanted Not immediately going to be prioritized — ask for mentoring instructions! label Nov 1, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement Something new the playground could do
Projects
None yet
Development

No branches or pull requests

2 participants