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

Enhancement: support .mlg files #118

Closed
jfehrle opened this issue Nov 27, 2018 · 5 comments
Closed

Enhancement: support .mlg files #118

jfehrle opened this issue Nov 27, 2018 · 5 comments

Comments

@jfehrle
Copy link
Collaborator

jfehrle commented Nov 27, 2018

plugin version: 0.67.2

Description Support .mlg files

.mlg files specify the grammar for a parser. They generally include a bunch of embedded OCaml. It would be great if syntax highlighting, comment a line/block and some of the other basic features worked in .mlg files.

Even better would be to populate the structure panel with the pure OCaml items that appear before GRAMMAR EXTEND Gram. And with a bit more work, maybe include grammar symbol definitions in the structure panel.

Here is an example .mlg file: https://github.com/coq/coq/blob/master/plugins/ltac/g_tactic.mlg

@giraud
Copy link
Owner

giraud commented Nov 27, 2018

done.
image

but the grammar section is totally foreign to me. is there any grammar 😉 that describe it ?

@jfehrle
Copy link
Collaborator Author

jfehrle commented Nov 27, 2018

Thanks, that's much better. The comment/uncomment operations don't work, though.

When I put in the request, I thought .mlg was a general-purpose format, but then I realized that it's specific to the Coq project. Whatever support you can provide would be great, but it may not be something you want to spend much time on.

Nonetheless, the grammar file is in https://github.com/coq/coq/tree/master/coqpp. Looks like coqpp_parse.mly is the yacc input file, coqpp_lex.mll is the lex input file.

It would also be helpful if the plugin supported .mll and .mly files to some degree--they are general purpose formats though I don't know how widely they're used in OCaml.

@giraud
Copy link
Owner

giraud commented Dec 15, 2018

I added some highlighting to mll mly.
if needed, create more specific issues, thanks.

@giraud giraud closed this as completed Dec 15, 2018
@giraud
Copy link
Owner

giraud commented Jun 20, 2023

Not working anymore in 0.113, need to implement the same host injection like what has been done in mll/mly

@giraud giraud reopened this Jun 20, 2023
@giraud
Copy link
Owner

giraud commented Jun 21, 2023

better parsing of mlg, with correct ocaml parser used in injection blocks. support syntax highlighting and folding.
image

giraud added a commit that referenced this issue Jun 21, 2023
giraud added a commit that referenced this issue Jul 4, 2023
@giraud giraud closed this as completed Aug 25, 2023
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

No branches or pull requests

2 participants