Skip to content

Commit

Permalink
fix surrounding brackets
Browse files Browse the repository at this point in the history
  • Loading branch information
abentkamp committed Dec 8, 2023
1 parent 314c834 commit 0b1d361
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion client/src/monacoSetup.ts
Original file line number Diff line number Diff line change
Expand Up @@ -36,9 +36,11 @@ export function monacoSetup () {
})

let config: any = { ...languageConfig }
config.autoClosingPairs = config.autoClosingPairs.map(
const translateBrackets = (f) => f.map(
pair => { return {'open': pair[0], 'close': pair[1]} }
)
config.autoClosingPairs = translateBrackets(config.autoClosingPairs)
config.surroundingPairs = translateBrackets(config.surroundingPairs)
monaco.languages.setLanguageConfiguration('lean4', config);

const registry = new Registry({
Expand Down

0 comments on commit 0b1d361

Please sign in to comment.