How to enable CodeMirror extension only for the target kernel/language

JupyterLab
1

I have written a CodeMirror extension to JupyterLab for syntax highlighting, it works well for my target kernel/language, but it changes the highlighting for other kernels/languages to this language. Any clue why this would happen? The relevant code are:

const plugin: JupyterFrontEndPlugin<void> = {
  id: 'jupyterlab-lean4-codemirror-extension:plugin',
  description: 'A JupyterLab extension for CodeMirror Lean 4 mode',
  autoStart: true,
  requires: [IEditorExtensionRegistry],
  activate: (app: JupyterFrontEnd, extensions: IEditorExtensionRegistry) => {
    extensions.addExtension(
      Object.freeze({
        name: 'codemirror:lean4',
        languages: [{
          name: 'lean4',
          mime: 'text/x-lean4',
          extensions: ['.lean']
        }],
        factory: () =>
          EditorExtensionRegistry.createConfigurableExtension(() =>
            [StreamLanguage.define(getLean4mode())]
          ),
      })
    );
    console.log('JupyterLab extension jupyterlab-lean4-codemirror-extension is activated!');
  }
2 Likes
2

When you register an extension using the IEditorExtensionRegistry token then it applies to all editors. What you want to do instead is to register a language using the IEditorLanguageRegistry token. It has addLanguage() method which accepts IEditorLanguage interface.

Feel free to ask any follow-up questions if you are stuck, it seems that (oddly) there is no example extension for this one.

3 Likes
3

Thanks for the prompt reply, it works like a charm! The relevant code has been changed to:

const plugin: JupyterFrontEndPlugin<void> = {
  id: 'jupyterlab-lean4-codemirror-extension:plugin',
  description: 'A JupyterLab extension for CodeMirror Lean 4 mode',
  autoStart: true,
  requires: [IEditorLanguageRegistry],
  activate: (app: JupyterFrontEnd, languages: IEditorLanguageRegistry) => {
    languages.addLanguage({
      name: 'lean4',
      mime: 'text/x-lean4',
      load: async () => new LanguageSupport(StreamLanguage.define(getLean4mode()))
    });
    console.log('JupyterLab extension jupyterlab-lean4-codemirror-extension is activated!');
  }
};

Full code: Integrate the extension into installation script and CI by utensil · Pull Request #2 · utensil/lean4_jupyter · GitHub

2 Likes