I don't have access to idris1 & it's pretty annoying to swtich between idris-mode and idris2-mode for testing so I figured I'd ask here: Would idris-mode benefit from a fix similar to https://github.com/idris-community/idris2-mode/pull/20 ?