Zulip Chat Archive
Stream: general
Topic: How to pass environment during `initialize`?
nrs (Nov 26 2024 at 02:14):
I'd like to write this bit of code at the top of my file: initialize discard <| registerParserCategory _ ``custom_parser ``customCat
where the typehole indicates the environment to which registerParserCategory
adds the custom_parser
attribute. How could I access the environment here to register this parser attribute? (context: I'm trying to implement an analog to @[term_parser]
and @[command_parser]
using my own syntax category)
nrs (Nov 26 2024 at 05:07):
the following might work. is it the only way? is there no way of doing this through initialize
?
elab "register_parser_cat" attrName:ident catName:ident : command => do
match attrName.raw, catName.raw with
| .ident _ _ namea _ , .ident _ _ nameb _ =>
let env <- getEnv
setEnv (<- registerParserCategory env namea nameb)
| _, _ => throwError "bad attrName or catName"
register_parser_cat customparser customCat
Last updated: May 02 2025 at 03:31 UTC