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