Closed virinchiv closed 6 months ago
It looks like this works correctly! Congratulations on finding the place to make the changes. A couple of suggestions:
var
(should be const
) replacements
to identify characters that should be replaced, and their replacements. Your code has [[ and ⟦, and ]] and ⟧, hard-coded. Of course, we know that (right now) [[
and ]]
are the only pair that we should be concerned with ... but it would be nicer if you would find them in the dictionary rather than hard-code them.
I changed the code in editor.js so that when the Autopair setting is turned on and two brackets '[[' are typed in, the replacement from '[[' to '⟦' occurs on the left side along with ']]' to '⟧' on the right side. Everything else operates same as before.