diff --git a/src/main/java/org/aya/intellij/actions/Commenter.kt b/src/main/java/org/aya/intellij/actions/Commenter.kt
index aa438e6..dbb6a22 100644
--- a/src/main/java/org/aya/intellij/actions/Commenter.kt
+++ b/src/main/java/org/aya/intellij/actions/Commenter.kt
@@ -3,7 +3,7 @@ package org.aya.intellij.actions
 import com.intellij.lang.CodeDocumentationAwareCommenterEx
 import com.intellij.psi.PsiComment
 import com.intellij.psi.PsiElement
-import org.aya.intellij.parser.AyaParserDefinition
+import org.aya.intellij.language.AyaParserDefinition
 import org.aya.intellij.psi.concrete.AyaPsiRemark
 
 class Commenter : CodeDocumentationAwareCommenterEx {
diff --git a/src/main/java/org/aya/intellij/actions/FindUsages.java b/src/main/java/org/aya/intellij/actions/FindUsages.java
index 2db4146..a1e3926 100644
--- a/src/main/java/org/aya/intellij/actions/FindUsages.java
+++ b/src/main/java/org/aya/intellij/actions/FindUsages.java
@@ -3,8 +3,8 @@
 import com.intellij.lang.cacheBuilder.WordsScanner;
 import com.intellij.lang.findUsages.FindUsagesProvider;
 import com.intellij.psi.PsiElement;
-import org.aya.intellij.parser.AyaParserDefinition;
-import org.aya.intellij.parser.AyaWordsScanner;
+import org.aya.intellij.language.AyaParserDefinition;
+import org.aya.intellij.language.AyaWordsScanner;
 import org.aya.intellij.psi.AyaPsiNamedElement;
 import org.aya.intellij.psi.concrete.*;
 import org.jetbrains.annotations.Nls;
diff --git a/src/main/java/org/aya/intellij/actions/ReferenceContributor.java b/src/main/java/org/aya/intellij/actions/ReferenceContributor.java
index fbe791b..24596eb 100644
--- a/src/main/java/org/aya/intellij/actions/ReferenceContributor.java
+++ b/src/main/java/org/aya/intellij/actions/ReferenceContributor.java
@@ -7,11 +7,11 @@
 import com.intellij.psi.*;
 import com.intellij.util.ProcessingContext;
 import org.aya.intellij.psi.AyaPsiElement;
+import org.aya.intellij.psi.AyaPsiReference;
 import org.aya.intellij.psi.concrete.AyaPsiAtomBindPattern;
 import org.aya.intellij.psi.concrete.AyaPsiNewArgField;
 import org.aya.intellij.psi.concrete.AyaPsiProjFixId;
 import org.aya.intellij.psi.concrete.AyaPsiRefExpr;
-import org.aya.intellij.psi.ref.AyaPsiReference;
 import org.jetbrains.annotations.NotNull;
 
 /**
diff --git a/src/main/java/org/aya/intellij/actions/SyntaxHighlight.kt b/src/main/java/org/aya/intellij/actions/SyntaxHighlight.kt
index 41c6a08..268e685 100644
--- a/src/main/java/org/aya/intellij/actions/SyntaxHighlight.kt
+++ b/src/main/java/org/aya/intellij/actions/SyntaxHighlight.kt
@@ -7,7 +7,7 @@ import com.intellij.openapi.editor.colors.TextAttributesKey
 import com.intellij.openapi.fileTypes.SyntaxHighlighterBase
 import com.intellij.psi.TokenType
 import com.intellij.psi.tree.IElementType
-import org.aya.intellij.parser.AyaParserDefinition
+import org.aya.intellij.language.AyaParserDefinition
 import org.aya.parser.AyaPsiElementTypes
 
 class SyntaxHighlight : SyntaxHighlighterBase() {
diff --git a/src/main/java/org/aya/intellij/lsp/AyaLsp.java b/src/main/java/org/aya/intellij/actions/lsp/AyaLsp.java
similarity index 98%
rename from src/main/java/org/aya/intellij/lsp/AyaLsp.java
rename to src/main/java/org/aya/intellij/actions/lsp/AyaLsp.java
index fee05b3..d7b0653 100644
--- a/src/main/java/org/aya/intellij/lsp/AyaLsp.java
+++ b/src/main/java/org/aya/intellij/actions/lsp/AyaLsp.java
@@ -1,4 +1,4 @@
-package org.aya.intellij.lsp;
+package org.aya.intellij.actions.lsp;
 
 import com.intellij.codeInsight.daemon.DaemonCodeAnalyzer;
 import com.intellij.openapi.diagnostic.Logger;
@@ -29,10 +29,11 @@
 import org.aya.concrete.stmt.Decl;
 import org.aya.concrete.stmt.Stmt;
 import org.aya.generic.Constants;
+import org.aya.intellij.language.AyaIJParserImpl;
 import org.aya.intellij.psi.AyaPsiElement;
 import org.aya.intellij.psi.AyaPsiFile;
 import org.aya.intellij.psi.AyaPsiNamedElement;
-import org.aya.intellij.psi.ref.AyaPsiReference;
+import org.aya.intellij.psi.AyaPsiReference;
 import org.aya.intellij.service.ProblemService;
 import org.aya.lsp.actions.GotoDefinition;
 import org.aya.lsp.server.AyaLanguageClient;
diff --git a/src/main/java/org/aya/intellij/lsp/AyaStartup.java b/src/main/java/org/aya/intellij/actions/lsp/AyaStartup.java
similarity index 96%
rename from src/main/java/org/aya/intellij/lsp/AyaStartup.java
rename to src/main/java/org/aya/intellij/actions/lsp/AyaStartup.java
index e2ed7bc..6a1470c 100644
--- a/src/main/java/org/aya/intellij/lsp/AyaStartup.java
+++ b/src/main/java/org/aya/intellij/actions/lsp/AyaStartup.java
@@ -1,4 +1,4 @@
-package org.aya.intellij.lsp;
+package org.aya.intellij.actions.lsp;
 
 import com.intellij.openapi.module.ModuleManager;
 import com.intellij.openapi.project.Project;
diff --git a/src/main/java/org/aya/intellij/lsp/JB.java b/src/main/java/org/aya/intellij/actions/lsp/JB.java
similarity index 98%
rename from src/main/java/org/aya/intellij/lsp/JB.java
rename to src/main/java/org/aya/intellij/actions/lsp/JB.java
index 5d57f35..c3f9329 100644
--- a/src/main/java/org/aya/intellij/lsp/JB.java
+++ b/src/main/java/org/aya/intellij/actions/lsp/JB.java
@@ -1,4 +1,4 @@
-package org.aya.intellij.lsp;
+package org.aya.intellij.actions.lsp;
 
 import com.intellij.diff.util.LineCol;
 import com.intellij.openapi.project.Project;
diff --git a/src/main/java/org/aya/intellij/run/AyaRunLineMarkerContributor.java b/src/main/java/org/aya/intellij/actions/run/AyaRunLineMarkerContributor.java
similarity index 95%
rename from src/main/java/org/aya/intellij/run/AyaRunLineMarkerContributor.java
rename to src/main/java/org/aya/intellij/actions/run/AyaRunLineMarkerContributor.java
index 24fcba7..8e2fb56 100644
--- a/src/main/java/org/aya/intellij/run/AyaRunLineMarkerContributor.java
+++ b/src/main/java/org/aya/intellij/actions/run/AyaRunLineMarkerContributor.java
@@ -1,4 +1,4 @@
-package org.aya.intellij.run;
+package org.aya.intellij.actions.run;
 
 import com.intellij.execution.lineMarker.ExecutorAction;
 import com.intellij.execution.lineMarker.RunLineMarkerContributor;
@@ -8,11 +8,11 @@
 import com.intellij.psi.PsiElement;
 import com.intellij.psi.tree.IElementType;
 import kala.collection.immutable.ImmutableSeq;
-import org.aya.intellij.AyaIcons;
 import org.aya.intellij.psi.AyaPsiFile;
 import org.aya.intellij.psi.concrete.AyaPsiDecl;
 import org.aya.intellij.psi.concrete.AyaPsiDeclNameOrInfix;
 import org.aya.intellij.psi.concrete.AyaPsiPrimName;
+import org.aya.intellij.ui.AyaIcons;
 import org.aya.parser.AyaPsiElementTypes;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
diff --git a/src/main/java/org/aya/intellij/run/TyckRunConfig.java b/src/main/java/org/aya/intellij/actions/run/TyckRunConfig.java
similarity index 99%
rename from src/main/java/org/aya/intellij/run/TyckRunConfig.java
rename to src/main/java/org/aya/intellij/actions/run/TyckRunConfig.java
index 19e51dc..df8ced6 100644
--- a/src/main/java/org/aya/intellij/run/TyckRunConfig.java
+++ b/src/main/java/org/aya/intellij/actions/run/TyckRunConfig.java
@@ -1,4 +1,4 @@
-package org.aya.intellij.run;
+package org.aya.intellij.actions.run;
 
 import com.intellij.execution.ExecutionException;
 import com.intellij.execution.Executor;
diff --git a/src/main/java/org/aya/intellij/run/TyckRunConfigEditorUI.form b/src/main/java/org/aya/intellij/actions/run/TyckRunConfigEditorUI.form
similarity index 96%
rename from src/main/java/org/aya/intellij/run/TyckRunConfigEditorUI.form
rename to src/main/java/org/aya/intellij/actions/run/TyckRunConfigEditorUI.form
index c662763..a48c431 100644
--- a/src/main/java/org/aya/intellij/run/TyckRunConfigEditorUI.form
+++ b/src/main/java/org/aya/intellij/actions/run/TyckRunConfigEditorUI.form
@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="UTF-8"?>
-<form xmlns="http://www.intellij.com/uidesigner/form/" version="1" bind-to-class="org.aya.intellij.run.TyckRunConfigEditorUI">
+<form xmlns="http://www.intellij.com/uidesigner/form/" version="1" bind-to-class="org.aya.intellij.actions.run.TyckRunConfigEditorUI">
   <grid id="27dc6" binding="root" layout-manager="GridLayoutManager" row-count="3" column-count="1" same-size-horizontally="false" same-size-vertically="false" hgap="-1" vgap="-1">
     <margin top="0" left="0" bottom="0" right="0"/>
     <constraints>
diff --git a/src/main/java/org/aya/intellij/run/TyckRunConfigEditorUI.java b/src/main/java/org/aya/intellij/actions/run/TyckRunConfigEditorUI.java
similarity index 97%
rename from src/main/java/org/aya/intellij/run/TyckRunConfigEditorUI.java
rename to src/main/java/org/aya/intellij/actions/run/TyckRunConfigEditorUI.java
index 1e8bba7..0f5a322 100644
--- a/src/main/java/org/aya/intellij/run/TyckRunConfigEditorUI.java
+++ b/src/main/java/org/aya/intellij/actions/run/TyckRunConfigEditorUI.java
@@ -1,4 +1,4 @@
-package org.aya.intellij.run;
+package org.aya.intellij.actions.run;
 
 import com.intellij.openapi.options.SettingsEditor;
 import com.intellij.openapi.ui.LabeledComponent;
diff --git a/src/main/java/org/aya/intellij/proof/ProofSearch.java b/src/main/java/org/aya/intellij/actions/search/ProofSearch.java
similarity index 96%
rename from src/main/java/org/aya/intellij/proof/ProofSearch.java
rename to src/main/java/org/aya/intellij/actions/search/ProofSearch.java
index f9518d1..87a6ede 100644
--- a/src/main/java/org/aya/intellij/proof/ProofSearch.java
+++ b/src/main/java/org/aya/intellij/actions/search/ProofSearch.java
@@ -1,4 +1,4 @@
-package org.aya.intellij.proof;
+package org.aya.intellij.actions.search;
 
 import com.intellij.ide.projectView.PresentationData;
 import com.intellij.openapi.project.Project;
@@ -10,11 +10,10 @@
 import org.aya.concrete.stmt.QualifiedID;
 import org.aya.core.term.Term;
 import org.aya.generic.util.InterruptException;
-import org.aya.intellij.AyaIcons;
-import org.aya.intellij.actions.SearchEverywhere;
-import org.aya.intellij.lsp.AyaIJParserImpl;
+import org.aya.intellij.language.AyaIJParserImpl;
 import org.aya.intellij.psi.AyaPsiElement;
 import org.aya.intellij.service.DistillerService;
+import org.aya.intellij.ui.AyaIcons;
 import org.aya.ref.DefVar;
 import org.aya.util.distill.DistillerOptions;
 import org.aya.util.error.SourcePos;
diff --git a/src/main/java/org/aya/intellij/proof/ProofSearchUI.kt b/src/main/java/org/aya/intellij/actions/search/ProofSearchUI.kt
similarity index 99%
rename from src/main/java/org/aya/intellij/proof/ProofSearchUI.kt
rename to src/main/java/org/aya/intellij/actions/search/ProofSearchUI.kt
index 3bd56b9..054b519 100644
--- a/src/main/java/org/aya/intellij/proof/ProofSearchUI.kt
+++ b/src/main/java/org/aya/intellij/actions/search/ProofSearchUI.kt
@@ -1,4 +1,4 @@
-package org.aya.intellij.proof
+package org.aya.intellij.actions.search
 
 import com.intellij.ide.actions.searcheverywhere.FoundItemDescriptor
 import com.intellij.ide.actions.searcheverywhere.SearchEverywhereContributorFactory
diff --git a/src/main/java/org/aya/intellij/actions/SearchEverywhere.java b/src/main/java/org/aya/intellij/actions/search/SearchEverywhere.java
similarity index 94%
rename from src/main/java/org/aya/intellij/actions/SearchEverywhere.java
rename to src/main/java/org/aya/intellij/actions/search/SearchEverywhere.java
index f4b294c..1e42d39 100644
--- a/src/main/java/org/aya/intellij/actions/SearchEverywhere.java
+++ b/src/main/java/org/aya/intellij/actions/search/SearchEverywhere.java
@@ -1,4 +1,4 @@
-package org.aya.intellij.actions;
+package org.aya.intellij.actions.search;
 
 import com.intellij.navigation.ChooseByNameContributorEx2;
 import com.intellij.navigation.NavigationItem;
@@ -13,12 +13,12 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.tuple.Tuple;
 import kala.tuple.Tuple2;
-import org.aya.intellij.AyaFileType;
-import org.aya.intellij.lsp.AyaLsp;
-import org.aya.intellij.lsp.JB;
+import org.aya.intellij.actions.lsp.AyaLsp;
+import org.aya.intellij.actions.lsp.JB;
+import org.aya.intellij.language.AyaFileType;
+import org.aya.intellij.psi.AyaNavItem;
 import org.aya.intellij.psi.AyaPsiFile;
 import org.aya.intellij.psi.AyaPsiGenericDecl;
-import org.aya.intellij.ui.AyaNavItem;
 import org.aya.ref.DefVar;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
diff --git a/src/main/java/org/aya/intellij/inspection/AyaInspection.kt b/src/main/java/org/aya/intellij/inspection/AyaInspection.kt
index 6169df4..ab25204 100644
--- a/src/main/java/org/aya/intellij/inspection/AyaInspection.kt
+++ b/src/main/java/org/aya/intellij/inspection/AyaInspection.kt
@@ -6,11 +6,11 @@ import com.intellij.codeInspection.ProblemsHolder
 import com.intellij.psi.PsiElementVisitor
 import com.intellij.util.IncorrectOperationException
 import org.aya.intellij.AyaBundle.message
+import org.aya.intellij.actions.lsp.AyaLsp
 import org.aya.intellij.inspection.error.ErrorInspection
 import org.aya.intellij.inspection.goal.GoalInspection
 import org.aya.intellij.inspection.info.InfoInspection
 import org.aya.intellij.inspection.warning.*
-import org.aya.intellij.lsp.AyaLsp
 
 abstract class AyaInspection : LocalInspectionTool() {
   override fun isEnabledByDefault() = true
diff --git a/src/main/java/org/aya/intellij/inspection/CatchAll.java b/src/main/java/org/aya/intellij/inspection/CatchAll.java
index 22ad59c..00aaafe 100644
--- a/src/main/java/org/aya/intellij/inspection/CatchAll.java
+++ b/src/main/java/org/aya/intellij/inspection/CatchAll.java
@@ -5,8 +5,8 @@
 import com.intellij.psi.PsiElementVisitor;
 import com.intellij.psi.PsiFile;
 import kala.collection.SeqView;
-import org.aya.intellij.lsp.AyaLsp;
-import org.aya.intellij.lsp.JB;
+import org.aya.intellij.actions.lsp.AyaLsp;
+import org.aya.intellij.actions.lsp.JB;
 import org.aya.intellij.psi.concrete.AyaPsiVisitor;
 import org.aya.intellij.service.DistillerService;
 import org.aya.util.reporter.Problem;
diff --git a/src/main/java/org/aya/intellij/inspection/error/ErrorInspection.java b/src/main/java/org/aya/intellij/inspection/error/ErrorInspection.java
index c9553e3..71290de 100644
--- a/src/main/java/org/aya/intellij/inspection/error/ErrorInspection.java
+++ b/src/main/java/org/aya/intellij/inspection/error/ErrorInspection.java
@@ -8,10 +8,10 @@
 import com.intellij.psi.PsiFile;
 import kala.collection.SeqView;
 import org.aya.intellij.AyaBundle;
+import org.aya.intellij.actions.lsp.AyaLsp;
+import org.aya.intellij.actions.lsp.JB;
 import org.aya.intellij.inspection.CatchAll;
 import org.aya.intellij.inspection.Jobs;
-import org.aya.intellij.lsp.AyaLsp;
-import org.aya.intellij.lsp.JB;
 import org.aya.intellij.psi.AyaPsiFile;
 import org.aya.intellij.service.DistillerService;
 import org.aya.util.reporter.Problem;
diff --git a/src/main/java/org/aya/intellij/inspection/goal/GoalInspection.kt b/src/main/java/org/aya/intellij/inspection/goal/GoalInspection.kt
index 1fa9c9e..0660d2b 100644
--- a/src/main/java/org/aya/intellij/inspection/goal/GoalInspection.kt
+++ b/src/main/java/org/aya/intellij/inspection/goal/GoalInspection.kt
@@ -6,8 +6,8 @@ import com.intellij.codeInspection.ProblemHighlightType
 import com.intellij.codeInspection.ProblemsHolder
 import com.intellij.openapi.project.Project
 import org.aya.intellij.AyaBundle
+import org.aya.intellij.actions.lsp.AyaLsp
 import org.aya.intellij.inspection.AyaInspection
-import org.aya.intellij.lsp.AyaLsp
 import org.aya.intellij.psi.concrete.AyaPsiHoleExpr
 import org.aya.intellij.psi.concrete.AyaPsiVisitor
 import org.aya.intellij.psi.utils.AyaPsiFactory
diff --git a/src/main/java/org/aya/intellij/inspection/info/InfoInspection.java b/src/main/java/org/aya/intellij/inspection/info/InfoInspection.java
index a8f8ab1..a0d6dff 100644
--- a/src/main/java/org/aya/intellij/inspection/info/InfoInspection.java
+++ b/src/main/java/org/aya/intellij/inspection/info/InfoInspection.java
@@ -4,8 +4,8 @@
 import com.intellij.psi.PsiFile;
 import kala.collection.SeqView;
 import org.aya.intellij.AyaBundle;
+import org.aya.intellij.actions.lsp.AyaLsp;
 import org.aya.intellij.inspection.CatchAll;
-import org.aya.intellij.lsp.AyaLsp;
 import org.aya.util.reporter.Problem;
 import org.jetbrains.annotations.NotNull;
 
diff --git a/src/main/java/org/aya/intellij/inspection/warning/BadCounterexampleInspection.kt b/src/main/java/org/aya/intellij/inspection/warning/BadCounterexampleInspection.kt
index 670116d..33d2be8 100644
--- a/src/main/java/org/aya/intellij/inspection/warning/BadCounterexampleInspection.kt
+++ b/src/main/java/org/aya/intellij/inspection/warning/BadCounterexampleInspection.kt
@@ -4,7 +4,7 @@ import com.intellij.codeInspection.*
 import com.intellij.openapi.project.Project
 import org.aya.concrete.error.BadCounterexampleWarn
 import org.aya.intellij.AyaBundle
-import org.aya.intellij.lsp.AyaLsp
+import org.aya.intellij.actions.lsp.AyaLsp
 import org.aya.intellij.psi.concrete.AyaPsiOpenKw
 import org.aya.intellij.psi.concrete.AyaPsiVisitor
 
diff --git a/src/main/java/org/aya/intellij/inspection/warning/BadModifierInspection.kt b/src/main/java/org/aya/intellij/inspection/warning/BadModifierInspection.kt
index 40d99e9..1da64c9 100644
--- a/src/main/java/org/aya/intellij/inspection/warning/BadModifierInspection.kt
+++ b/src/main/java/org/aya/intellij/inspection/warning/BadModifierInspection.kt
@@ -4,7 +4,7 @@ import com.intellij.codeInspection.*
 import com.intellij.openapi.project.Project
 import org.aya.concrete.error.BadModifierWarn
 import org.aya.intellij.AyaBundle
-import org.aya.intellij.lsp.AyaLsp
+import org.aya.intellij.actions.lsp.AyaLsp
 import org.aya.intellij.psi.concrete.AyaPsiFnModifiers
 import org.aya.intellij.psi.concrete.AyaPsiVisitor
 
diff --git a/src/main/java/org/aya/intellij/inspection/warning/DominationInspection.kt b/src/main/java/org/aya/intellij/inspection/warning/DominationInspection.kt
index 2bfeb7d..3aa623f 100644
--- a/src/main/java/org/aya/intellij/inspection/warning/DominationInspection.kt
+++ b/src/main/java/org/aya/intellij/inspection/warning/DominationInspection.kt
@@ -3,7 +3,7 @@ package org.aya.intellij.inspection.warning
 import com.intellij.codeInspection.*
 import com.intellij.openapi.project.Project
 import org.aya.intellij.AyaBundle
-import org.aya.intellij.lsp.AyaLsp
+import org.aya.intellij.actions.lsp.AyaLsp
 import org.aya.intellij.psi.AyaPsiElement
 import org.aya.intellij.psi.concrete.AyaPsiBareClause
 import org.aya.intellij.psi.concrete.AyaPsiBarredClause
diff --git a/src/main/java/org/aya/intellij/inspection/warning/NamingInspection.kt b/src/main/java/org/aya/intellij/inspection/warning/NamingInspection.kt
index d8a5166..d87e64a 100644
--- a/src/main/java/org/aya/intellij/inspection/warning/NamingInspection.kt
+++ b/src/main/java/org/aya/intellij/inspection/warning/NamingInspection.kt
@@ -4,7 +4,7 @@ import com.intellij.codeInsight.daemon.impl.quickfix.RenameElementFix
 import com.intellij.codeInspection.ProblemHighlightType
 import com.intellij.codeInspection.ProblemsHolder
 import org.aya.intellij.AyaBundle
-import org.aya.intellij.lsp.AyaLsp
+import org.aya.intellij.actions.lsp.AyaLsp
 import org.aya.intellij.psi.AyaPsiElement
 import org.aya.intellij.psi.AyaPsiNamedElement
 import org.aya.intellij.psi.concrete.AyaPsiVisitor
diff --git a/src/main/java/org/aya/intellij/inspection/warning/WarningInspection.java b/src/main/java/org/aya/intellij/inspection/warning/WarningInspection.java
index 8c273ac..d884074 100644
--- a/src/main/java/org/aya/intellij/inspection/warning/WarningInspection.java
+++ b/src/main/java/org/aya/intellij/inspection/warning/WarningInspection.java
@@ -4,9 +4,9 @@
 import com.intellij.psi.PsiFile;
 import kala.collection.SeqView;
 import org.aya.intellij.AyaBundle;
+import org.aya.intellij.actions.lsp.AyaLsp;
 import org.aya.intellij.inspection.CatchAll;
 import org.aya.intellij.inspection.Jobs;
-import org.aya.intellij.lsp.AyaLsp;
 import org.aya.util.reporter.Problem;
 import org.jetbrains.annotations.NotNull;
 
diff --git a/src/main/java/org/aya/intellij/lsp/AyaIJParserImpl.java b/src/main/java/org/aya/intellij/language/AyaIJParserImpl.java
similarity index 97%
rename from src/main/java/org/aya/intellij/lsp/AyaIJParserImpl.java
rename to src/main/java/org/aya/intellij/language/AyaIJParserImpl.java
index 9eb0d83..b43b429 100644
--- a/src/main/java/org/aya/intellij/lsp/AyaIJParserImpl.java
+++ b/src/main/java/org/aya/intellij/language/AyaIJParserImpl.java
@@ -1,4 +1,4 @@
-package org.aya.intellij.lsp;
+package org.aya.intellij.language;
 
 import com.intellij.lang.ASTNode;
 import com.intellij.openapi.application.ApplicationManager;
@@ -14,6 +14,7 @@
 import org.aya.concrete.Expr;
 import org.aya.concrete.GenericAyaParser;
 import org.aya.concrete.stmt.Stmt;
+import org.aya.intellij.actions.lsp.JB;
 import org.aya.intellij.psi.AyaPsiElement;
 import org.aya.intellij.psi.AyaPsiFile;
 import org.aya.intellij.psi.utils.AyaPsiFactory;
diff --git a/src/main/java/org/aya/intellij/parser/AyaNamesValidator.java b/src/main/java/org/aya/intellij/language/AyaNamesValidator.java
similarity index 98%
rename from src/main/java/org/aya/intellij/parser/AyaNamesValidator.java
rename to src/main/java/org/aya/intellij/language/AyaNamesValidator.java
index 41529b7..fffd0ab 100644
--- a/src/main/java/org/aya/intellij/parser/AyaNamesValidator.java
+++ b/src/main/java/org/aya/intellij/language/AyaNamesValidator.java
@@ -1,4 +1,4 @@
-package org.aya.intellij.parser;
+package org.aya.intellij.language;
 
 import com.intellij.lang.refactoring.NamesValidator;
 import com.intellij.openapi.project.Project;
diff --git a/src/main/java/org/aya/intellij/parser/AyaParserDefinition.java b/src/main/java/org/aya/intellij/language/AyaParserDefinition.java
similarity index 98%
rename from src/main/java/org/aya/intellij/parser/AyaParserDefinition.java
rename to src/main/java/org/aya/intellij/language/AyaParserDefinition.java
index 9c13ea4..4525605 100644
--- a/src/main/java/org/aya/intellij/parser/AyaParserDefinition.java
+++ b/src/main/java/org/aya/intellij/language/AyaParserDefinition.java
@@ -1,4 +1,4 @@
-package org.aya.intellij.parser;
+package org.aya.intellij.language;
 
 import com.intellij.lang.ASTNode;
 import com.intellij.lexer.FlexAdapter;
diff --git a/src/main/java/org/aya/intellij/parser/AyaWordsScanner.java b/src/main/java/org/aya/intellij/language/AyaWordsScanner.java
similarity index 99%
rename from src/main/java/org/aya/intellij/parser/AyaWordsScanner.java
rename to src/main/java/org/aya/intellij/language/AyaWordsScanner.java
index 7a395e9..2bab684 100644
--- a/src/main/java/org/aya/intellij/parser/AyaWordsScanner.java
+++ b/src/main/java/org/aya/intellij/language/AyaWordsScanner.java
@@ -13,7 +13,7 @@
  * See the License for the specific language governing permissions and
  * limitations under the License.
  */
-package org.aya.intellij.parser;
+package org.aya.intellij.language;
 
 import com.intellij.lang.cacheBuilder.VersionedWordsScanner;
 import com.intellij.lang.cacheBuilder.WordOccurrence;
diff --git a/src/main/java/org/aya/intellij/language.kt b/src/main/java/org/aya/intellij/language/language.kt
similarity index 85%
rename from src/main/java/org/aya/intellij/language.kt
rename to src/main/java/org/aya/intellij/language/language.kt
index 246c87e..e69a598 100644
--- a/src/main/java/org/aya/intellij/language.kt
+++ b/src/main/java/org/aya/intellij/language/language.kt
@@ -1,7 +1,8 @@
-package org.aya.intellij
+package org.aya.intellij.language
 
 import com.intellij.openapi.fileTypes.LanguageFileType
 import org.aya.generic.Constants
+import org.aya.intellij.ui.AyaIcons
 import org.aya.parser.AyaLanguage
 
 object AyaFileType : LanguageFileType(AyaLanguage.INSTANCE) {
diff --git a/src/main/java/org/aya/intellij/ui/utils.kt b/src/main/java/org/aya/intellij/psi/AyaNavItem.kt
similarity index 88%
rename from src/main/java/org/aya/intellij/ui/utils.kt
rename to src/main/java/org/aya/intellij/psi/AyaNavItem.kt
index 39b7918..0f2aafb 100644
--- a/src/main/java/org/aya/intellij/ui/utils.kt
+++ b/src/main/java/org/aya/intellij/psi/AyaNavItem.kt
@@ -1,8 +1,7 @@
-package org.aya.intellij.ui
+package org.aya.intellij.psi
 
 import com.intellij.navigation.NavigationItem
 import com.intellij.pom.Navigatable
-import org.aya.intellij.psi.AyaPsiElement
 
 /**
  * Provide flexible (the verbose flag) presentation control over psi elements.
diff --git a/src/main/java/org/aya/intellij/psi/AyaPsiElement.java b/src/main/java/org/aya/intellij/psi/AyaPsiElement.java
index 0c38eb8..7d86676 100644
--- a/src/main/java/org/aya/intellij/psi/AyaPsiElement.java
+++ b/src/main/java/org/aya/intellij/psi/AyaPsiElement.java
@@ -6,8 +6,8 @@
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.concrete.stmt.QualifiedID;
-import org.aya.intellij.AyaIcons;
 import org.aya.intellij.psi.concrete.*;
+import org.aya.intellij.ui.AyaIcons;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
diff --git a/src/main/java/org/aya/intellij/psi/AyaPsiFile.java b/src/main/java/org/aya/intellij/psi/AyaPsiFile.java
index e24cd0c..ba950eb 100644
--- a/src/main/java/org/aya/intellij/psi/AyaPsiFile.java
+++ b/src/main/java/org/aya/intellij/psi/AyaPsiFile.java
@@ -7,7 +7,7 @@
 import com.intellij.psi.FileViewProvider;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
-import org.aya.intellij.AyaFileType;
+import org.aya.intellij.language.AyaFileType;
 import org.aya.parser.AyaLanguage;
 import org.jetbrains.annotations.NotNull;
 
diff --git a/src/main/java/org/aya/intellij/psi/AyaPsiNamedElement.java b/src/main/java/org/aya/intellij/psi/AyaPsiNamedElement.java
index f41df25..6f03a94 100644
--- a/src/main/java/org/aya/intellij/psi/AyaPsiNamedElement.java
+++ b/src/main/java/org/aya/intellij/psi/AyaPsiNamedElement.java
@@ -2,7 +2,7 @@
 
 import com.intellij.psi.PsiNameIdentifierOwner;
 import org.aya.concrete.stmt.QualifiedID;
-import org.aya.intellij.lsp.AyaLsp;
+import org.aya.intellij.actions.lsp.AyaLsp;
 import org.aya.lsp.utils.ModuleVar;
 import org.aya.ref.DefVar;
 import org.aya.ref.LocalVar;
diff --git a/src/main/java/org/aya/intellij/psi/ref/AyaPsiReference.java b/src/main/java/org/aya/intellij/psi/AyaPsiReference.java
similarity index 92%
rename from src/main/java/org/aya/intellij/psi/ref/AyaPsiReference.java
rename to src/main/java/org/aya/intellij/psi/AyaPsiReference.java
index 4889b49..0666fdc 100644
--- a/src/main/java/org/aya/intellij/psi/ref/AyaPsiReference.java
+++ b/src/main/java/org/aya/intellij/psi/AyaPsiReference.java
@@ -1,4 +1,4 @@
-package org.aya.intellij.psi.ref;
+package org.aya.intellij.psi;
 
 import com.intellij.openapi.util.NlsSafe;
 import com.intellij.openapi.util.TextRange;
@@ -6,9 +6,7 @@
 import com.intellij.psi.PsiReferenceBase;
 import com.intellij.util.IncorrectOperationException;
 import org.aya.intellij.actions.ReferenceContributor;
-import org.aya.intellij.lsp.AyaLsp;
-import org.aya.intellij.psi.AyaPsiElement;
-import org.aya.intellij.psi.AyaPsiNamedElement;
+import org.aya.intellij.actions.lsp.AyaLsp;
 import org.aya.intellij.psi.concrete.AyaPsiAtomBindPattern;
 import org.aya.intellij.psi.concrete.AyaPsiNewArgField;
 import org.aya.intellij.psi.concrete.AyaPsiProjFixId;
diff --git a/src/main/java/org/aya/intellij/AyaIcons.java b/src/main/java/org/aya/intellij/ui/AyaIcons.java
similarity index 97%
rename from src/main/java/org/aya/intellij/AyaIcons.java
rename to src/main/java/org/aya/intellij/ui/AyaIcons.java
index 1ed5e49..2dcb1be 100644
--- a/src/main/java/org/aya/intellij/AyaIcons.java
+++ b/src/main/java/org/aya/intellij/ui/AyaIcons.java
@@ -1,4 +1,4 @@
-package org.aya.intellij;
+package org.aya.intellij.ui;
 
 import com.intellij.icons.AllIcons;
 import com.intellij.openapi.util.IconLoader;
diff --git a/src/main/java/org/aya/intellij/ui/settings/AyaColorSettingsPage.java b/src/main/java/org/aya/intellij/ui/settings/AyaColorSettingsPage.java
index 339db9b..483e535 100644
--- a/src/main/java/org/aya/intellij/ui/settings/AyaColorSettingsPage.java
+++ b/src/main/java/org/aya/intellij/ui/settings/AyaColorSettingsPage.java
@@ -6,8 +6,8 @@
 import com.intellij.openapi.options.colors.ColorDescriptor;
 import com.intellij.openapi.options.colors.ColorSettingsPage;
 import com.intellij.openapi.util.NlsContexts;
-import org.aya.intellij.AyaIcons;
 import org.aya.intellij.actions.SyntaxHighlight;
+import org.aya.intellij.ui.AyaIcons;
 import org.aya.parser.AyaLanguage;
 import org.jetbrains.annotations.NonNls;
 import org.jetbrains.annotations.NotNull;
diff --git a/src/main/java/org/aya/intellij/ui/toolwindow/AyaToolWindow.java b/src/main/java/org/aya/intellij/ui/toolwindow/AyaToolWindow.java
index 7df26dd..bb3be59 100644
--- a/src/main/java/org/aya/intellij/ui/toolwindow/AyaToolWindow.java
+++ b/src/main/java/org/aya/intellij/ui/toolwindow/AyaToolWindow.java
@@ -3,8 +3,8 @@
 import com.intellij.openapi.project.Project;
 import com.intellij.openapi.wm.ToolWindow;
 import com.intellij.openapi.wm.ToolWindowFactory;
-import org.aya.intellij.AyaIcons;
 import org.aya.intellij.service.ProblemService;
+import org.aya.intellij.ui.AyaIcons;
 import org.jetbrains.annotations.NotNull;
 
 public class AyaToolWindow implements ToolWindowFactory {
diff --git a/src/main/java/org/aya/intellij/ui/toolwindow/GoalsView.java b/src/main/java/org/aya/intellij/ui/toolwindow/GoalsView.java
index 068afbd..3d871f9 100644
--- a/src/main/java/org/aya/intellij/ui/toolwindow/GoalsView.java
+++ b/src/main/java/org/aya/intellij/ui/toolwindow/GoalsView.java
@@ -18,12 +18,12 @@
 import org.aya.core.term.ErrorTerm;
 import org.aya.core.term.Term;
 import org.aya.intellij.AyaBundle;
-import org.aya.intellij.AyaIcons;
-import org.aya.intellij.lsp.AyaLsp;
-import org.aya.intellij.lsp.JB;
+import org.aya.intellij.actions.lsp.AyaLsp;
+import org.aya.intellij.actions.lsp.JB;
 import org.aya.intellij.psi.AyaPsiFile;
 import org.aya.intellij.psi.concrete.AyaPsiHoleExpr;
 import org.aya.intellij.service.ProblemService;
+import org.aya.intellij.ui.AyaIcons;
 import org.aya.intellij.ui.AyaTreeView;
 import org.aya.pretty.doc.Doc;
 import org.aya.tyck.error.Goal;
diff --git a/src/main/resources/META-INF/plugin.xml b/src/main/resources/META-INF/plugin.xml
index 43d88e1..37876cd 100644
--- a/src/main/resources/META-INF/plugin.xml
+++ b/src/main/resources/META-INF/plugin.xml
@@ -9,18 +9,18 @@
 
   <extensions defaultExtensionNs="com.intellij">
     <postStartupActivity
-      implementation="org.aya.intellij.lsp.AyaStartup"/>
+      implementation="org.aya.intellij.actions.lsp.AyaStartup"/>
 
     <fileType
       name="Aya File"
-      implementationClass="org.aya.intellij.AyaFileType"
+      implementationClass="org.aya.intellij.language.AyaFileType"
       language="Aya"
       extensions="aya"/>
 
     <!-- language features -->
     <lang.parserDefinition
       language="Aya"
-      implementationClass="org.aya.intellij.parser.AyaParserDefinition"/>
+      implementationClass="org.aya.intellij.language.AyaParserDefinition"/>
     <lang.findUsagesProvider
       language="Aya"
       implementationClass="org.aya.intellij.actions.FindUsages"/>
@@ -29,10 +29,10 @@
       implementationClass="org.aya.intellij.actions.RefactoringSupport"/>
     <lang.namesValidator
       language="Aya"
-      implementationClass="org.aya.intellij.parser.AyaNamesValidator"/>
+      implementationClass="org.aya.intellij.language.AyaNamesValidator"/>
     <lang.syntaxHighlighterFactory
       language="Aya"
-      implementationClass="org.aya.intellij.parser.AyaParserDefinition$SyntaxHighlightFactory"/>
+      implementationClass="org.aya.intellij.language.AyaParserDefinition$SyntaxHighlightFactory"/>
     <lang.braceMatcher
       language="Aya"
       implementationClass="org.aya.intellij.actions.BraceMatcher"/>
@@ -53,17 +53,17 @@
     <psi.referenceContributor
       implementation="org.aya.intellij.actions.ReferenceContributor"/>
     <navbar implementation="org.aya.intellij.ui.structure.AyaNavBar"/>
-    <gotoSymbolContributor implementation="org.aya.intellij.actions.SearchEverywhere$Symbol"/>
-    <searchEverywhereContributor implementation="org.aya.intellij.proof.ProofSearchContributorFactory"/>
+    <gotoSymbolContributor implementation="org.aya.intellij.actions.search.SearchEverywhere$Symbol"/>
+    <searchEverywhereContributor implementation="org.aya.intellij.actions.search.ProofSearchContributorFactory"/>
 
     <!-- run configuration -->
     <configurationType
-      implementation="org.aya.intellij.run.TyckRunConfig$Type"/>
+      implementation="org.aya.intellij.actions.run.TyckRunConfig$Type"/>
     <runConfigurationProducer
-      implementation="org.aya.intellij.run.TyckRunConfig$Producer"/>
+      implementation="org.aya.intellij.actions.run.TyckRunConfig$Producer"/>
     <runLineMarkerContributor
       language="Aya"
-      implementationClass="org.aya.intellij.run.AyaRunLineMarkerContributor"/>
+      implementationClass="org.aya.intellij.actions.run.AyaRunLineMarkerContributor"/>
 
     <!-- settings -->
     <applicationConfigurable
diff --git a/src/test/kotlin/proof-search.kt b/src/test/kotlin/proof-search.kt
index f63358e..0cdc4fe 100644
--- a/src/test/kotlin/proof-search.kt
+++ b/src/test/kotlin/proof-search.kt
@@ -1,6 +1,6 @@
 import com.intellij.testFramework.fixtures.BasePlatformTestCase
 import junit.framework.TestCase
-import org.aya.intellij.proof.ProofSearch
+import org.aya.intellij.actions.search.ProofSearch
 
 class ProofSearchParserTest : BasePlatformTestCase() {
   fun `test wildcard matches any id`() = "_".matches("hello")