From 462e52d0c0c276e89713d54fffdc1767335570fa Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 22 Oct 2024 12:07:37 +0200 Subject: [PATCH] feat: use "eureka!" icon for theorem completions (#5801) It's difficult to distinguish theorems from regular definitions in the completion menu, which is annoying when using completion for searching one or the other. This PR makes theorem completions use the "Eureka!" icon (![eureka icon](https://code.visualstudio.com/assets/docs/editor/intellisense/symbol-event.svg)) to distinguish them more clearly from other completions. NB: We are very limited in terms of which icons we can pick here since [the completion kinds provided by LSP / VS Code](https://code.visualstudio.com/docs/editor/intellisense#_types-of-completions) are optimized for object-oriented programming languages, but I think this choice strikes a nice balance between being easy to identify, having some visual connection to theorem proving and not being used a lot in other languages and thus not clashing with pre-existing associations. --- src/Lean/Declaration.lean | 4 +++ src/Lean/Server/Completion.lean | 2 ++ .../interactive/completion2.lean.expected.out | 30 +++++++++---------- .../completionFallback.lean.expected.out | 4 +-- .../completionPrv.lean.expected.out | 12 ++++---- .../travellingCompletions.lean.expected.out | 4 +-- 6 files changed, 31 insertions(+), 25 deletions(-) diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 4be29c4134..b764111dda 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -472,6 +472,10 @@ def isInductive : ConstantInfo → Bool | inductInfo _ => true | _ => false +def isTheorem : ConstantInfo → Bool + | thmInfo _ => true + | _ => false + def inductiveVal! : ConstantInfo → InductiveVal | .inductInfo val => val | _ => panic! "Expected a `ConstantInfo.inductInfo`." diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index bb0829f4b0..83a38dac54 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -207,6 +207,8 @@ private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionIt return CompletionItemKind.enum else return CompletionItemKind.struct + else if constInfo.isTheorem then + return CompletionItemKind.event else if (← isProjectionFn constInfo.name) then return CompletionItemKind.field else if (← whnf constInfo.type).isForall then diff --git a/tests/lean/interactive/completion2.lean.expected.out b/tests/lean/interactive/completion2.lean.expected.out index 6e34e10334..3f9aafd094 100644 --- a/tests/lean/interactive/completion2.lean.expected.out +++ b/tests/lean/interactive/completion2.lean.expected.out @@ -3,7 +3,7 @@ {"items": [{"sortText": "0", "label": "ax1", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -11,7 +11,7 @@ "id": {"const": {"declName": "Foo.Bla.ax1"}}}}, {"sortText": "1", "label": "ex1", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -19,7 +19,7 @@ "id": {"const": {"declName": "Foo.Bla.ex1"}}}}, {"sortText": "2", "label": "ex2", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -27,7 +27,7 @@ "id": {"const": {"declName": "Foo.Bla.ex2"}}}}, {"sortText": "3", "label": "ex3", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -39,7 +39,7 @@ {"items": [{"sortText": "0", "label": "ax1", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -47,7 +47,7 @@ "id": {"const": {"declName": "Foo.Bla.ax1"}}}}, {"sortText": "1", "label": "ex1", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -55,7 +55,7 @@ "id": {"const": {"declName": "Foo.Bla.ex1"}}}}, {"sortText": "2", "label": "ex2", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -63,7 +63,7 @@ "id": {"const": {"declName": "Foo.Bla.ex2"}}}}, {"sortText": "3", "label": "ex3", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -75,7 +75,7 @@ {"items": [{"sortText": "0", "label": "ax1", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -83,7 +83,7 @@ "id": {"const": {"declName": "Foo.Bla.ax1"}}}}, {"sortText": "1", "label": "ex1", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -91,7 +91,7 @@ "id": {"const": {"declName": "Foo.Bla.ex1"}}}}, {"sortText": "2", "label": "ex2", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -99,7 +99,7 @@ "id": {"const": {"declName": "Foo.Bla.ex2"}}}}, {"sortText": "3", "label": "ex3", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -111,7 +111,7 @@ {"items": [{"sortText": "0", "label": "ex1", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -119,7 +119,7 @@ "id": {"const": {"declName": "Foo.Bla.ex1"}}}}, {"sortText": "1", "label": "ex2", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, @@ -127,7 +127,7 @@ "id": {"const": {"declName": "Foo.Bla.ex2"}}}}, {"sortText": "2", "label": "ex3", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completion2.lean"}, diff --git a/tests/lean/interactive/completionFallback.lean.expected.out b/tests/lean/interactive/completionFallback.lean.expected.out index 7cd2e288a0..0d524243dc 100644 --- a/tests/lean/interactive/completionFallback.lean.expected.out +++ b/tests/lean/interactive/completionFallback.lean.expected.out @@ -55,7 +55,7 @@ {"items": [{"sortText": "0", "label": "ha", - "kind": 5, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completionFallback.lean"}, @@ -63,7 +63,7 @@ "id": {"const": {"declName": "CustomAnd.ha"}}}}, {"sortText": "1", "label": "hb", - "kind": 5, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completionFallback.lean"}, diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out index 6c62ec4e39..ac03b62acc 100644 --- a/tests/lean/interactive/completionPrv.lean.expected.out +++ b/tests/lean/interactive/completionPrv.lean.expected.out @@ -31,7 +31,7 @@ "id": {"const": {"declName": "instToBoolBool"}}}}, {"sortText": "2", "label": "BitVec.getElem_ofBoolListBE", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, @@ -39,7 +39,7 @@ "id": {"const": {"declName": "BitVec.getElem_ofBoolListBE"}}}}, {"sortText": "3", "label": "BitVec.getLsbD_ofBoolListBE", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, @@ -47,7 +47,7 @@ "id": {"const": {"declName": "BitVec.getLsbD_ofBoolListBE"}}}}, {"sortText": "4", "label": "BitVec.getMsbD_ofBoolListBE", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, @@ -55,7 +55,7 @@ "id": {"const": {"declName": "BitVec.getMsbD_ofBoolListBE"}}}}, {"sortText": "5", "label": "BitVec.ofBool_and_ofBool", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, @@ -63,7 +63,7 @@ "id": {"const": {"declName": "BitVec.ofBool_and_ofBool"}}}}, {"sortText": "6", "label": "BitVec.ofBool_or_ofBool", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, @@ -71,7 +71,7 @@ "id": {"const": {"declName": "BitVec.ofBool_or_ofBool"}}}}, {"sortText": "7", "label": "BitVec.ofBool_xor_ofBool", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, diff --git a/tests/lean/interactive/travellingCompletions.lean.expected.out b/tests/lean/interactive/travellingCompletions.lean.expected.out index 46409f6f6b..15c1f442e7 100644 --- a/tests/lean/interactive/travellingCompletions.lean.expected.out +++ b/tests/lean/interactive/travellingCompletions.lean.expected.out @@ -39,7 +39,7 @@ {"items": [{"sortText": "0", "label": "continuousAdd", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///travellingCompletions.lean"}, @@ -47,7 +47,7 @@ "id": {"const": {"declName": "Prod.continuousAdd"}}}}, {"sortText": "1", "label": "continuousSMul", - "kind": 3, + "kind": 23, "data": {"params": {"textDocument": {"uri": "file:///travellingCompletions.lean"},