Activate extension on language 'idris2' too

[Release-Candidate]

Hi, would it be a problem if you automatically activate the extension on Idris 2 files too? That means adding

"activationEvents": [
    "onLanguage:idris2",
    "onLanguage:idris",

to package.json.

If you want to, I could generate a pull request for that.

[Release-Candidate]

Just adding the the language activation of idris2 is actually not enough to get the extension to work with files marked as idris2.

[meraymond2]

Hi,

it should activate anything that ends in .idr, which covers Idris and Idris 2. That's configured here. What file extension are you using?

[Release-Candidate]

Sorry, I haven't stated the problem clearly. The Idris2 LSP extension defines the language idris2 for .idr files and only supports this (not the language idris) but your extension only supports the language idris. So to be able to use both at the same time either the LSP extension could use the language idris instead of idris2 or your extension could support the language idris2 too when in Idris 2 mode. My pull request of adding the language idris2 to the supported ones in your extension is working for me and it shouldn't have any side effects on Idris 2 files that have the language idris associated with them.

Your extension's language definition in package.json:

 "languages": [
      {
        "id": "idris",
        "aliases": [
          "Idris",
          "idris"
        ],
        "configuration": "./language-configuration.json",
        "extensions": [
          ".idr"
        ]
      },

The one of the LSP package.json:

"languages": [
      {
        "id": "idris2",
        "aliases": [
          "Idris 2",
          "idris2",
          "idris"
        ],
        "extensions": [
          ".idr"
        ],
        "configuration": "./language-configuration.json"
      },

[meraymond2]

My pull request of adding the language idris2 to the supported ones in your extension is working for me

Apologies if I've misunderstood, but for the purposes of this extension, it doesn't matter if I call the 'language', in the vscode sense, idris or idris2. Both map to the same language-configuration.json and textmate grammar.

I guess it does matter in terms of the extension tags. If you search for Idris 2, this one doesn't come up, even though it does support it.

[Release-Candidate]

The support of the VS Code language idris2 is only needed to be able to use this extension and the Idris2 LSP extension at the same time. Which I (and maybe others) like to do, because your extension still has some features (like autocomplete and display of documentation) that the LSP is missing at this time. Thank you for your work!

[meraymond2]

Cool, that makes sense. I want to test it when I have a chance (hopefully this weekend) and then I'll see about merging it.