Fix #444

src/main/kotlin/org/arend/ArendStartupActivity.kt

@@ -1,5 +1,7 @@
 package org.arend
 
+import com.intellij.codeInsight.editorActions.SelectionQuotingTypedHandler
+import com.intellij.codeInsight.editorActions.TypedHandlerDelegate
 import com.intellij.openapi.actionSystem.ActionManager
 import com.intellij.openapi.application.ApplicationManager
 import com.intellij.openapi.application.runReadAction
@@ -83,6 +85,7 @@ class ArendStartupActivity : ProjectActivity {
         actionManager?.getAction(ArendBundle.message("arend.disableActionUnmark"))?.let {
             actionManager.unregisterAction(ArendBundle.message("arend.disableActionUnmark"))
         }
+        TypedHandlerDelegate.EP_NAME.point.unregisterExtension(SelectionQuotingTypedHandler::class.java)
     }
 
     private fun changeColors() {

src/main/kotlin/org/arend/codeInsight/ArendTypedHandler.kt

@@ -2,23 +2,65 @@ package org.arend.codeInsight
 
 import com.intellij.codeInsight.AutoPopupController
 import com.intellij.codeInsight.CodeInsightSettings
+import com.intellij.codeInsight.editorActions.SelectionQuotingTypedHandler
 import com.intellij.codeInsight.editorActions.TypedHandlerDelegate
 import com.intellij.openapi.components.service
 import com.intellij.openapi.editor.Editor
 import com.intellij.openapi.project.Project
 import com.intellij.psi.PsiDocumentManager
 import com.intellij.psi.PsiFile
 import com.intellij.util.text.CharArrayCharSequence
+import org.arend.psi.ArendElementTypes.*
 import org.arend.settings.ArendSettings
 import org.arend.psi.ArendFile
+import org.arend.psi.childOfType
+import org.arend.psi.ext.ArendCompositeElementImpl
 
 
 class ArendTypedHandler : TypedHandlerDelegate() {
+
+    private fun changeCorrespondingElement(c: Char, project: Project, editor: Editor, file: PsiFile) {
+        val parent = file.findElementAt(editor.selectionModel.selectionStart)
+            ?.parent as? ArendCompositeElementImpl?
+
+        val correspondingElementOffset = when (c) {
+            '(' -> parent?.childOfType(RBRACE)?.textOffset
+            '{' -> parent?.childOfType(RPAREN)?.textOffset
+            ')' -> parent?.childOfType(LBRACE)?.textOffset
+            else -> parent?.childOfType(LPAREN)?.textOffset
+        } ?: return
+
+        val document = editor.document
+        PsiDocumentManager.getInstance(project).commitDocument(document)
+
+        document.replaceString(
+            correspondingElementOffset,
+            correspondingElementOffset + 1,
+            when (c) {
+                '(' -> ")"
+                '{' -> "}"
+                ')' -> "("
+                else -> "{"
+            }
+        )
+    }
+
+    override fun beforeSelectionRemoved(c: Char, project: Project, editor: Editor, file: PsiFile): Result {
+        if (PARENTHESES_AND_BRACES.contains(c.toString())) {
+            val selectedText = editor.selectionModel.selectedText
+            if (PARENTHESES_AND_BRACES.contains(selectedText)) {
+                changeCorrespondingElement(c, project, editor, file)
+                return Result.CONTINUE
+            }
+        }
+        return SelectionQuotingTypedHandler().beforeSelectionRemoved(c, project, editor, file)
+    }
+
     override fun charTyped(c: Char, project: Project, editor: Editor, file: PsiFile): Result {
         if (file !is ArendFile) {
             return super.charTyped(c, project, editor, file)
         }
-        if (c == '{' || c == '(') {
+        if (PARENTHESES_AND_BRACES.contains(c.toString())) {
             return Result.STOP // To prevent auto-formatting
         }
 
@@ -62,4 +104,7 @@ class ArendTypedHandler : TypedHandlerDelegate() {
         } else {
             Result.CONTINUE
         }
-}
+
+}
+
+private val PARENTHESES_AND_BRACES = listOf("(", "{", ")", "}")

src/test/kotlin/org/arend/codeInsight/ArendTypedHandlerTest.kt

@@ -0,0 +1,28 @@
+package org.arend.codeInsight
+
+import org.arend.ArendTestBase
+
+class ArendTypedHandlerTest : ArendTestBase() {
+    private fun check(code: String, newCode: String, type: Char) {
+        InlineFile(code).withCaret()
+        myFixture.performEditorAction("EditorSelectWord")
+        myFixture.type(type)
+        myFixture.checkResult(newCode)
+    }
+
+    fun `test parens`() = check("""\func f {-caret-}(a : Nat) => {?}""", """\func f {a : Nat} => {?}""", '{')
+
+    fun `test braces`() = check("""\func f {-caret-}{a : Nat} => {?}""", """\func f (a : Nat) => {?}""", '(')
+
+    fun `test nothing`() = check("""\func f {-caret-}(a : Nat} => {?}""", """\func f {a : Nat} => {?}""", '{')
+
+    fun `test nothing 2`() = check("""\func f {-caret-}(a : Nat} => {?}""", """\func f *a : Nat} => {?}""", '*')
+
+    fun `test simple quoting parens`() = check("""\func f (a {-caret-}: Nat} => {?}""", """\func f (a (:) Nat} => {?}""", '(')
+
+    fun `test simple quoting braces`() = check("""\func f (a {-caret-}: Nat} => {?}""", """\func f (a {:} Nat} => {?}""", '{')
+
+    fun `test closing paren`() = check("""\func f (a : Nat){-caret-} => {?}""", """\func f {a : Nat} => {?}""", '}')
+
+    fun `test closing brace`() = check("""\func f {a : Nat}{-caret-} => {?}""", """\func f (a : Nat) => {?}""", ')')
+}