max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: use "eureka!" icon for theorem completions (#5801)

Browse source 
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.
This commit is contained in:
Marc Huisinga 2024-10-22 12:07:37 +02:00 • committed by GitHub
parent d0abe1d382
commit 462e52d0c0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 31 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Declaration.lean
View file

@ -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`."

2
src/Lean/Server/Completion.lean
View file

@ -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

30
tests/lean/interactive/completion2.lean.expected.out
View file

@ -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"},

4
tests/lean/interactive/completionFallback.lean.expected.out
View file

@ -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"},

12
tests/lean/interactive/completionPrv.lean.expected.out
View file

@ -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"},

4
tests/lean/interactive/travellingCompletions.lean.expected.out
View file

@ -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"},