Merge pull request #536 from alex999990009/alex99999/fixes

Fix exceptions, visual texts and a menu item in the toolbar

src/main/kotlin/org/arend/actions/ArendCreateFileAction.kt

@@ -35,6 +35,6 @@ class ArendCreateFileAction : CreateFileFromTemplateAction(CAPTION, "", ArendIco
     }
 
     private companion object {
-        private const val CAPTION = "New Arend File"
+        private const val CAPTION = "Arend File"
     }
 }

src/main/kotlin/org/arend/actions/mark/ArendMarkActionUtils.kt

@@ -5,7 +5,8 @@ import com.intellij.ide.projectView.actions.MarkRootActionBase
 import com.intellij.openapi.actionSystem.AnActionEvent
 import com.intellij.openapi.actionSystem.CommonDataKeys
 import com.intellij.openapi.actionSystem.LangDataKeys
-import com.intellij.openapi.application.ApplicationManager
+import com.intellij.openapi.application.invokeLater
+import com.intellij.openapi.application.runWriteAction
 import com.intellij.openapi.module.Module
 import com.intellij.openapi.roots.*
 import com.intellij.openapi.vfs.LocalFileSystem
@@ -44,8 +45,12 @@ private fun getDirByType(directoryType: DirectoryType, arendModuleConfigService:
 }
 
 private fun commitModel(module: Module?, model: ModifiableRootModel?) {
-    ApplicationManager.getApplication().runWriteAction { model?.commit() }
-    module?.project?.let { SaveAndSyncHandler.getInstance().scheduleProjectSave(it) }
+    invokeLater {
+        runWriteAction {
+            model?.commit()
+        }
+        module?.project?.let { SaveAndSyncHandler.getInstance().scheduleProjectSave(it) }
+    }
 }
 
 internal fun removeOldFolder(virtualFile: VirtualFile?, arendModuleConfigService: ArendModuleConfigService?, directoryType: DirectoryType) {

src/main/kotlin/org/arend/intention/ReplaceBracketsIntention.kt

@@ -6,13 +6,14 @@ import com.intellij.openapi.editor.Editor
 import com.intellij.openapi.project.Project
 import com.intellij.psi.PsiDocumentManager
 import com.intellij.psi.PsiElement
+import com.intellij.psi.util.elementType
 import com.intellij.refactoring.suggested.startOffset
 import org.arend.psi.ArendElementTypes.*
 import org.arend.psi.childOfType
 import org.arend.psi.ext.ArendCompositeElement
 import org.arend.util.ArendBundle
 
-class ReplaceBracketsIntention : SelfTargetingIntention<PsiElement>(PsiElement::class.java,  ArendBundle.message("arend.replaceBrackets")) {
+class ReplaceBracketsIntention : SelfTargetingIntention<PsiElement>(PsiElement::class.java, ArendBundle.message("arend.replaceBrackets")) {
 
     private fun getBrackets(element: PsiElement): Pair<PsiElement?, PsiElement?> {
         var currentElement: PsiElement? = element
@@ -33,6 +34,11 @@ class ReplaceBracketsIntention : SelfTargetingIntention<PsiElement>(PsiElement::
 
     override fun isApplicableTo(element: PsiElement, caretOffset: Int, editor: Editor): Boolean {
         val (left, right) = getBrackets(element)
+        text = if (left.elementType == LPAREN) {
+            ArendBundle.message("arend.replaceBrackets")
+        } else {
+            ArendBundle.message("arend.replaceParentheses")
+        }
         return left == element || right == element
     }
 

src/main/kotlin/org/arend/psi/listener/ArendPsiChangeService.kt

@@ -22,8 +22,10 @@ class ArendPsiChangeService {
     }
 
     fun updateDefinition(def: PsiConcreteReferable, file: ArendFile, isExternalUpdate: Boolean) {
-        for (listener in listeners) {
-            listener.updateDefinition(def, file, isExternalUpdate)
+        synchronized(listeners) {
+            for (listener in listeners) {
+                listener.updateDefinition(def, file, isExternalUpdate)
+            }
         }
     }
-}
+}

src/main/kotlin/org/arend/yaml/YamlFileService.kt

@@ -1,5 +1,7 @@
 package org.arend.yaml
 
+import com.intellij.openapi.application.ApplicationManager
+import com.intellij.openapi.module.Module
 import com.intellij.openapi.module.ModuleUtilCore
 import com.intellij.openapi.project.Project
 import com.intellij.openapi.vfs.VirtualFile

src/main/kotlin/org/arend/yaml/YamlNotificationProvider.kt

@@ -1,5 +1,6 @@
 package org.arend.yaml
 
+import com.intellij.openapi.application.ApplicationManager
 import com.intellij.openapi.components.service
 import com.intellij.openapi.fileEditor.FileEditor
 import com.intellij.openapi.project.Project
@@ -28,7 +29,13 @@ class YamlNotificationProvider : EditorNotificationProvider {
         panel.createActionLabel(ArendBundle.message("arend.updateYamlConfiguration")) {
             panel.isVisible = false
             yamlFileService.removeChangedFile(file)
-            yamlFileService.updateIdea(file)
+            ApplicationManager.getApplication().run {
+                executeOnPooledThread {
+                    runReadAction {
+                        yamlFileService.updateIdea(file)
+                    }
+                }
+            }
         }
         return panel
     }

src/main/resources/META-INF/plugin.xml

@@ -553,13 +553,6 @@
             <add-to-group group-id="GoToTargetEx" anchor="last" />
         </action>
 
-        <action class="org.arend.search.proof.ArendProofSearchAction"
-                text="Proof Search"
-                description="Run search for pattern expression in functions' signature">
-            <add-to-group group-id="SearchEverywhereActions" anchor="last" />
-            <keyboard-shortcut keymap="$default" first-keystroke="control alt P" />
-        </action>
-
         <group id="ToolbarArendGroup"
                class="org.arend.actions.ArendToolbarGroup"
                text="Arend Editor Toolbar"
@@ -586,6 +579,11 @@
                     class="org.arend.toolWindow.repl.ArendShowReplAction"
                     text="Show Arend REPL"
                     description="Display the Arend REPL as a tool window"/>
+            <action class="org.arend.search.proof.ArendProofSearchAction"
+                    text="Proof Search"
+                    description="Run search for pattern expression in functions' signature">
+                <keyboard-shortcut keymap="$default" first-keystroke="control alt P" />
+            </action>
             <add-to-group group-id="ToolsMenu" anchor="last" />
         </group>
 

src/main/resources/inspectionDescriptions/UnresolvedArendPattern.html

@@ -1,5 +1,5 @@
 <html>
 <body>
-Reports patterns that don't resolve into constructors
+Reports patterns that do not resolve into constructors
 </body>
 </html>

src/main/resources/intentionDescriptions/ReplaceBracketsIntention/description.html

@@ -1,5 +1,5 @@
 <html>
 <body>
-Replaces the brackets associated with this element from "(" and ") to "{" and "}" and vice versa
+Replaces the brackets or the parentheses associated with this element from "(" and ") to "{" and "}" and vice versa
 </body>
 </html>

src/main/resources/messages/ArendBundle.properties

@@ -199,7 +199,8 @@ arend.refactoring.move.unspecifiedPartOfTheClass=Unspecified part of the class
 arend.changeSignature.ambientError=Typechecking error in the expression or its parent
 arend.changeSignature.parseError=Unable to parse expression correctly
 
-arend.replaceBrackets=Replace the brackets
+arend.replaceBrackets=Replace with brackets
+arend.replaceParentheses=Replace with parentheses
 
 arend.updateYamlConfigurationQuestion=Would you like to update the settings from the YAML file?
 arend.updateYamlConfiguration=Update

src/test/kotlin/org/arend/intention/ReplaceBracketsIntentionTest.kt

@@ -4,15 +4,17 @@ import org.arend.quickfix.QuickFixTestBase
 import org.arend.util.ArendBundle
 
 class ReplaceBracketsIntentionTest : QuickFixTestBase() {
-    private val fixName = ArendBundle.message("arend.replaceBrackets")
-    private fun doTest(contents: String, result: String) = simpleQuickFixTest(fixName, contents, result)
+    private val fixNameBrackets = ArendBundle.message("arend.replaceBrackets")
+    private val fixNameParentheses = ArendBundle.message("arend.replaceParentheses")
+    private fun doTestBrackets(contents: String, result: String) = simpleQuickFixTest(fixNameBrackets, contents, result)
+    private fun doTestParentheses(contents: String, result: String) = simpleQuickFixTest(fixNameParentheses, contents, result)
 
-    fun testReplaceBrackets1() = doTest(
+    fun testReplaceBrackets() = doTestBrackets(
         """\func foo ({-caret-}a : Nat) => 1""",
         """\func foo {a : Nat} => 1"""
     )
 
-    fun testReplaceBrackets2() = doTest(
+    fun testReplaceParentheses() = doTestParentheses(
         """
             \func foo (a : Nat) => 1
             \func bar => foo {{-caret-}foo 0}