Joachim Breitner
232a0495b0
chore: remove public section from end of files ( #10684 )
...
This PR removes `public section` lines from end of files; they look a
bit silly there.
2025-10-06 13:30:48 +00:00
Sebastian Ullrich
ff1d3138bf
refactor: module-ize Lean ( #9330 )
2025-07-25 12:02:51 +00:00
Leonardo de Moura
88fbe2e531
chore: missing prelude
2024-02-25 11:44:42 -08:00
Scott Morrison
3dd10654e1
chore: upstream Std.CodeAction.*
...
Remove tactic_code_action
rearrange
oops
.
add tests
import file
Update src/Lean/Elab/Tactic/GuardMsgs.lean
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Update src/Lean/Elab/Tactic/GuardMsgs.lean
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
fix namespace
move GuardMsgs
cleanup
2024-02-25 11:44:42 -08:00
Sebastian Ullrich
f1a3169424
fix: [builtin_code_action_provider]
2024-02-20 12:48:19 +01:00
Henrik Böving
23e49eb519
perf: add prelude to all Lean modules
2024-02-18 14:55:17 -08:00
Sebastian Ullrich
55402a5899
feat: add [builtin_code_action_provider] ( #3289 )
2024-02-09 11:51:40 +00:00
Mario Carneiro
ad4b822734
fix: use snake case for @[code_action_provider]
2023-05-08 22:25:48 +02:00
Gabriel Ebner
041307fd4b
fix: build
2022-10-20 12:42:32 -07:00
E.W.Ayers
46112a5f2a
fix: review
2022-10-20 11:20:42 -07:00
E.W.Ayers
c9a26596dc
refactor: switch resolve to double eval strategy
...
Using option (2) from this comment:
https://github.com/leanprover/lean4/pull/1661#pullrequestreview-1135363727
2022-10-20 11:20:42 -07:00
E.W.Ayers
691835037e
feat: code action resolvers
2022-10-20 11:20:42 -07:00
E.W.Ayers
297d06fc0c
fix: issue where code action was not running
2022-10-20 11:20:42 -07:00
E.W.Ayers
c795e2b073
fix: rm CodeActionData
2022-10-20 11:20:42 -07:00
Ed Ayers
7f47a34656
style: apply suggestions from code review
...
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2022-10-20 11:20:42 -07:00
E.W.Ayers
260e42b0a7
doc: fix docs from review
2022-10-20 11:20:42 -07:00
E.W.Ayers
8085ce88e9
feat: CodeActionProvider
...
This is a low-level system for registering LSP code actions.
Developers can register their own code actions.
In future commits I am going to add features on top of this.
2022-10-20 11:20:42 -07:00
