[ misc ] Cleanup some files

grammar/voile.bnf

@@ -43,8 +43,8 @@ expr ::=
  | telescopicExpr
  | parenExpr
 
-piExpr ::= expr ARROW expr
-sigExpr ::= expr SIG expr
+piExpr ::= expr ARROW expr { mixin='org.ice1000.tt.psi.voile.VoilePiSigMixin '}
+sigExpr ::= expr SIG expr { mixin='org.ice1000.tt.psi.voile.VoilePiSigMixin '}
 telescopicExpr ::= LPAREN nameDecl+ COLON expr RPAREN {
 	pin=3
 	implements=['com.intellij.psi.PsiNameIdentifierOwner']

res/META-INF/change-notes.html

@@ -1,8 +1,9 @@
 0.5.1<br/>
 <ul>
 	<li>Voile code insight: parser, lexer, commenter, brace matcher,
-		syntax highlighter, color settings page
+		syntax highlighter, color settings page, reference resolving
 	</li>
+	<li>Cleanup some files</li>
 </ul>
 0.5.0<br/>
 <ul>

res/META-INF/description.html

@@ -66,6 +66,7 @@ <h3>Features (listed for each supported language):</h3><br/>
 			<li>Live templates context</li>
 			<li>Commenter, brace matcher</li>
 			<li>Syntax highlight, color settings page</li>
+			<li>Completion/find usages/goto declaration</li>
 			<li>Create and iconify files</li>
 		</ul>
 	</li>

res/META-INF/plugin.xml

@@ -45,6 +45,7 @@
 		<lang.braceMatcher language="Voile" implementationClass="org.ice1000.tt.editing.voile.VoileBraceMatcher"/>
 		<lang.refactoringSupport language="Voile" implementationClass="org.ice1000.tt.editing.InplaceRenameRefactoringSupportProvider"/>
 		<colorSettingsPage implementation="org.ice1000.tt.editing.voile.VoileColorSettingsPage"/>
+		<annotator language="Voile" implementationClass="org.ice1000.tt.editing.voile.VoileAnnotator"/>
 
 		<!--Agda-->
 		<configurationType implementation="org.ice1000.tt.execution.AgdaRunConfigurationType"/>

src/org/ice1000/tt/editing/acore/editing.kt

@@ -1,13 +1,16 @@
 package org.ice1000.tt.editing.acore
 
+import com.intellij.codeInspection.ProblemHighlightType
 import com.intellij.lang.BracePair
+import com.intellij.lang.annotation.AnnotationHolder
+import com.intellij.lang.annotation.Annotator
 import com.intellij.lang.cacheBuilder.DefaultWordsScanner
+import com.intellij.psi.PsiElement
 import com.intellij.psi.tree.TokenSet
+import org.ice1000.tt.TTBundle
 import org.ice1000.tt.editing.TTBraceMatcher
 import org.ice1000.tt.editing.TTFindUsagesProvider
-import org.ice1000.tt.psi.acore.ACoreTokenType
-import org.ice1000.tt.psi.acore.ACoreTypes
-import org.ice1000.tt.psi.acore.acoreLexer
+import org.ice1000.tt.psi.acore.*
 
 class ACoreBraceMatcher : TTBraceMatcher() {
 	private companion object Pairs {
@@ -21,3 +24,31 @@ class ACoreFindUsagesProvider : TTFindUsagesProvider() {
 	override fun getWordsScanner() = DefaultWordsScanner(acoreLexer(), ACoreTokenType.IDENTIFIERS, ACoreTokenType.COMMENTS, TokenSet.EMPTY)
 }
 
+class ACoreAnnotator : Annotator {
+	override fun annotate(element: PsiElement, holder: AnnotationHolder) {
+		when (element) {
+			is ACoreDeclaration -> declaration(element, holder)
+			is ACoreVariable -> variable(element, holder)
+		}
+	}
+
+	private fun variable(element: ACoreVariable, holder: AnnotationHolder) {
+		val resolution = element.reference?.resolve()
+		if (resolution == null) holder.createErrorAnnotation(element, TTBundle.message("tt.lint.unresolved")).apply {
+			textAttributes = ACoreHighlighter.UNRESOLVED
+			highlightType = ProblemHighlightType.LIKE_UNKNOWN_SYMBOL
+		}
+	}
+
+	private fun pattern(pattern: ACorePattern, holder: AnnotationHolder) {
+		when (pattern) {
+			is ACoreAtomPattern -> holder.createInfoAnnotation(pattern, null)
+				.textAttributes = ACoreHighlighter.FUNCTION_NAME
+			is ACorePairPattern -> pattern.patternList.forEach { pattern(it, holder) }
+		}
+	}
+
+	private fun declaration(element: ACoreDeclaration, holder: AnnotationHolder) {
+		element.pattern?.let { pattern(it, holder) }
+	}
+}

src/org/ice1000/tt/editing/agda/editing.kt

@@ -1,8 +1,19 @@
 package org.ice1000.tt.editing.agda
 
+import com.intellij.codeInsight.completion.CompletionContributor
+import com.intellij.codeInsight.completion.CompletionType
 import com.intellij.lang.BracePair
+import com.intellij.lang.annotation.AnnotationHolder
+import com.intellij.lang.annotation.Annotator
+import com.intellij.openapi.project.DumbAware
+import com.intellij.patterns.PlatformPatterns
+import com.intellij.psi.PsiElement
+import icons.TTIcons
+import org.ice1000.tt.editing.SimpleProvider
 import org.ice1000.tt.editing.TTBraceMatcher
-import org.ice1000.tt.psi.agda.AgdaTypes
+import org.ice1000.tt.editing.makeKeywordsCompletion
+import org.ice1000.tt.psi.agda.*
+import org.ice1000.tt.psi.childrenWithLeaves
 
 class AgdaBraceMatcher : TTBraceMatcher() {
 	private companion object Pairs {
@@ -15,3 +26,46 @@ class AgdaBraceMatcher : TTBraceMatcher() {
 
 	override fun getPairs() = PAIRS
 }
+
+class AgdaAnnotator : Annotator {
+	override fun annotate(element: PsiElement, holder: AnnotationHolder) {
+		when (element) {
+			is AgdaSignature -> signature(element, holder)
+			is AgdaVisibility, is AgdaRenaming -> rename(element, holder)
+			is AgdaRenamePair -> renamingPair(element, holder)
+		}
+	}
+
+	private fun renamingPair(element: AgdaRenamePair, holder: AnnotationHolder) {
+		val to = element.childrenWithLeaves.firstOrNull { it.text == "to" } ?: return
+		holder.createInfoAnnotation(to, null).textAttributes = AgdaHighlighter.KEYWORD
+	}
+
+	private fun rename(element: PsiElement, holder: AnnotationHolder) {
+		holder.createInfoAnnotation(element.firstChild, null).textAttributes = AgdaHighlighter.KEYWORD
+	}
+
+	private fun signature(element: AgdaSignature, holder: AnnotationHolder) {
+		if (element.parent !is AgdaLayout) return
+		element.nameDeclList.forEach {
+			holder.createInfoAnnotation(it, null)
+				.textAttributes = AgdaHighlighter.FUNCTION_NAME
+		}
+	}
+}
+
+class AgdaCompletionContributor : CompletionContributor(), DumbAware {
+	private val keywords = makeKeywordsCompletion(TTIcons.AGDA, listOf(
+		"no-eta-equality", "eta-equality",
+		"quoteContext", "constructor", "coinductive", "unquoteDecl", "unquoteDef",
+		"postulate", "primitive", "inductive", "quoteGoal", "quoteTerm",
+		"variable", "abstract", "instance", "rewrite", "private", "overlap",
+		"unquote", "pattern", "import", "module", "codata", "record", "infixl",
+		"infixr", "mutual", "forall", "tactic", "syntax", "where", "field",
+		"infix", "macro", "quote", "with", "open", "data", "let", "in", "do"
+	))
+
+	init {
+		extend(CompletionType.BASIC, PlatformPatterns.psiElement(), SimpleProvider(keywords))
+	}
+}

src/org/ice1000/tt/editing/cubicaltt/editing.kt

@@ -1,13 +1,14 @@
 package org.ice1000.tt.editing.cubicaltt
 
 import com.intellij.lang.BracePair
+import com.intellij.lang.annotation.AnnotationHolder
+import com.intellij.lang.annotation.Annotator
 import com.intellij.lang.cacheBuilder.DefaultWordsScanner
+import com.intellij.psi.PsiElement
 import com.intellij.psi.tree.TokenSet
 import org.ice1000.tt.editing.TTBraceMatcher
 import org.ice1000.tt.editing.TTFindUsagesProvider
-import org.ice1000.tt.psi.cubicaltt.CubicalTTTokenType
-import org.ice1000.tt.psi.cubicaltt.CubicalTTTypes
-import org.ice1000.tt.psi.cubicaltt.cubicalTTLexer
+import org.ice1000.tt.psi.cubicaltt.*
 
 class CubicalTTBraceMatcher : TTBraceMatcher() {
 	private companion object Pairs {
@@ -25,3 +26,22 @@ class CubicalTTBraceMatcher : TTBraceMatcher() {
 class CubicalTTFindUsagesProvider : TTFindUsagesProvider() {
 	override fun getWordsScanner() = DefaultWordsScanner(cubicalTTLexer(), CubicalTTTokenType.IDENTIFIERS, CubicalTTTokenType.COMMENTS, TokenSet.EMPTY)
 }
+
+class CubicalTTAnnotator : Annotator {
+	override fun annotate(element: PsiElement, holder: AnnotationHolder) {
+		when (element) {
+			is CubicalTTDecl -> decl(element, holder)
+			is CubicalTTData -> data(element, holder)
+		}
+	}
+
+	private fun data(element: CubicalTTData, holder: AnnotationHolder) {
+		val name = element.nameDecl ?: return
+		holder.createInfoAnnotation(name, null).textAttributes = CubicalTTHighlighter.FUNCTION_NAME
+	}
+
+	private fun decl(element: CubicalTTDecl, holder: AnnotationHolder) {
+		val name = element.firstChild as? CubicalTTNameDecl ?: return
+		holder.createInfoAnnotation(name, null).textAttributes = CubicalTTHighlighter.FUNCTION_NAME
+	}
+}