fix: guard against lean language id (#738)

Author: mhuisi

vscode-lean4/package.json

@@ -47,7 +47,8 @@
                 "lean4.input.languages": {
                     "type": "array",
                     "default": [
-                        "lean4"
+                        "lean4",
+                        "lean"
                     ],
                     "markdownDescription": "Enable Lean Unicode input in other file types.",
                     "items": {

vscode-lean4/src/abbreviation/VSCodeAbbreviationConfig.ts

@@ -24,7 +24,7 @@ export class VSCodeAbbreviationConfig implements AbbreviationConfig, Disposable
     private reloadConfig() {
         this.inputModeEnabled = workspace.getConfiguration('lean4.input').get('enabled', true)
         this.abbreviationCharacter = workspace.getConfiguration('lean4.input').get('leader', '\\')
-        this.languages = workspace.getConfiguration('lean4.input').get('languages', ['lean4'])
+        this.languages = workspace.getConfiguration('lean4.input').get('languages', ['lean4', 'lean'])
         this.customTranslations = workspace.getConfiguration('lean4.input').get('customTranslations', {})
         this.eagerReplacementEnabled = workspace.getConfiguration('lean4.input').get('eagerReplacementEnabled', true)
     }

vscode-lean4/src/extension.ts

@@ -22,7 +22,7 @@ import { ExtUri, extUriToCwdUri, FileUri, toExtUri } from './utils/exturi'
 import { FullInstaller } from './utils/fullInstaller'
 import { displayInternalErrorsIn } from './utils/internalErrors'
 import { registerLeanCommandRunner } from './utils/leanCmdRunner'
-import { lean, registerLeanEditorProviders, text } from './utils/leanEditorProvider'
+import { isLeanDocument, lean, registerLeanEditorProviders, text } from './utils/leanEditorProvider'
 import { LeanInstaller } from './utils/leanInstaller'
 import { ModuleTreeViewProvider } from './utils/moduleTreeViewProvider'
 import {
@@ -48,7 +48,7 @@ async function findInitialLeanProjectUri(editor: TextEditor): Promise<ExtUri | u
     if (info.kind === 'FileNotFound') {
         return undefined
     }
-    if (editor.document.languageId !== 'lean4' && info.kind === 'Success' && info.toolchainUri === undefined) {
+    if (!isLeanDocument(editor.document) && info.kind === 'Success' && info.toolchainUri === undefined) {
         return undefined
     }
     return info.projectRootUri
@@ -179,7 +179,7 @@ function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabled
 
     const checkForExtensionConflict = (doc: TextDocument) => {
         const isLean3ExtensionInstalled = extensions.getExtension('jroesch.lean') !== undefined
-        if (isLean3ExtensionInstalled && (doc.languageId === 'lean' || doc.languageId === 'lean4')) {
+        if (isLean3ExtensionInstalled && isLeanDocument(doc)) {
             displayNotification(
                 'Error',
                 "The Lean 3 and the Lean 4 VS Code extension are enabled at the same time. Since both extensions act on .lean files, this can lead to issues with either extension. Please disable the extension for the Lean major version that you do not wish to use ('Extensions' in the left sidebar > Cog icon > 'Disable').",
@@ -316,14 +316,14 @@ async function tryActivatingLean4Features(
         )
     }
     // We try activating the Lean features in two cases:
-    // 1. When revealing a new editor with the `lean4` language ID (e.g.: switching tabs, opening a new Lean document, changing the language ID to `lean4`)
-    // 2. When revealing a new editor in a Lean project that doesn't have the `lean4` language ID (e.g.: switching tabs, opening a new document)
+    // 1. When revealing a new editor with the `lean` or `lean4` language ID (e.g.: switching tabs, opening a new Lean document, changing the language ID to `lean` or `lean4`)
+    // 2. When revealing a new editor in a Lean project that doesn't have the `lean` or `lean4` language ID (e.g.: switching tabs, opening a new document)
     // These two events are disjoint, so combining them won't cause duplicate triggers.
     const combinedEvent = combine(
         lean.onDidRevealLeanEditor,
         _ => true,
         text.onDidRevealLeanEditor,
-        editor => editor.editor.document.languageId !== 'lean4',
+        editor => !isLeanDocument(editor.editor.document),
     )
     context.subscriptions.push(combinedEvent.disposable)
     context.subscriptions.push(

vscode-lean4/src/leanclient.ts

@@ -841,7 +841,7 @@ export class LeanClient implements Disposable {
         return {
             outputChannel: this.outputChannel,
             revealOutputChannelOn: RevealOutputChannelOn.Never, // contrary to the name, this disables the message boxes
-            documentSelector: [documentSelector],
+            documentSelector: [documentSelector, { ...documentSelector, language: 'lean' }],
             workspaceFolder,
             initializationOptions: {
                 hasWidgets: true,

vscode-lean4/src/utils/leanEditorProvider.ts

@@ -14,6 +14,10 @@ import {
 import { ExtUri, isExtUri, toExtUriOrError } from './exturi'
 import { groupByKey, groupByUniqueKey } from './groupBy'
 
+export function isLeanDocument(doc: TextDocument): boolean {
+    return isExtUri(doc.uri) && (doc.languageId === 'lean4' || doc.languageId === 'lean')
+}
+
 export class LeanDocument {
     constructor(
         readonly doc: TextDocument,
@@ -329,7 +333,7 @@ export class LeanEditorProvider implements Disposable {
     private isLeanDocument(doc: TextDocument): boolean {
         switch (this.mode) {
             case 'Lean':
-                return isExtUri(doc.uri) && doc.languageId === 'lean4'
+                return isLeanDocument(doc)
             case 'Text':
                 return isExtUri(doc.uri)
         }