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

Support for "New LF file" #112

Merged
merged 6 commits into from
Apr 27, 2023
Merged

Support for "New LF file" #112

merged 6 commits into from
Apr 27, 2023

Conversation

jesslin02
Copy link
Contributor

@jesslin02 jesslin02 commented Apr 23, 2023

addresses #48. clicking "New file" now includes an option to create a new LF file with the associated highlighting. like other languages, this new file will remain untitled until saved by the user, and the .lf extension will automatically be suggested when saving.

@jesslin02
Copy link
Contributor Author

image

not sure if we have a preference for "New Lingua Franca File" as pictured above vs just "Lingua Franca File".

@jesslin02 jesslin02 marked this pull request as ready for review April 24, 2023 06:39
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see that you did a few package upgrades, which is fine, but I'm a but surprised about the large number of lines that disappeared from the lock file. This might be completely benign, but I'm curious whether @petervdonovan has anything to say about this.

@lhstrh
Copy link
Member

lhstrh commented Apr 27, 2023

I tried it, and it works! Really nice! 🚀

Copy link
Contributor

@petervdonovan petervdonovan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. I am not worried about the lock file.

@lhstrh lhstrh changed the title adding LF to "New file" Support for "New LF file" Apr 27, 2023
@lhstrh lhstrh merged commit 985a4b8 into lf-lang:main Apr 27, 2023
@lhstrh lhstrh mentioned this pull request May 6, 2023
@lhstrh lhstrh added the feature label Aug 28, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants