df23b79c90
This PR fixes a bug where tactic auto-completion would produce tactic completion items in the entire trailing whitespace of an empty tactic block. Since #13229 further restricted top-level `by` blocks to be indentation- sensitive, this PR adjusts the logic to only display completion items at a "proper" indentation level. Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
135 lines
2.9 KiB
Text
135 lines
2.9 KiB
Text
prelude
|
|
import Init.Notation
|
|
|
|
/-
|
|
This test is a bit brittle because it checks that tactic completion works correctly for all
|
|
tactic completions that we get in `prelude` + `import Init.Notation`.
|
|
When changing the docstring of any of these tactics, this test will break.
|
|
|
|
If you didn't touch the elaboration infrastructure or the language server, then you can safely
|
|
assume that this test is still correct and unbreak it by overwriting
|
|
`completionTactics.lean.expected.out` with `completionTactics.lean.produced.out` after running
|
|
this test.
|
|
-/
|
|
|
|
/-- A docstring -/
|
|
syntax (name := skip) "skip" : tactic
|
|
|
|
/-- Another docstring -/
|
|
syntax (name := exact) "exact " term : tactic
|
|
|
|
example : True := by -- No completions expected
|
|
--^ completion
|
|
|
|
example : True := by -- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True := by ski -- Tactic completions matching `ski` expected
|
|
--^ completion
|
|
|
|
example : True := by skip -- No completions expected
|
|
--^ completion
|
|
|
|
example : True := by skip; -- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True := by skip; -- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True := by
|
|
skip
|
|
skip; -- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True := by
|
|
-- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True := by
|
|
skip
|
|
-- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True := by
|
|
-- All tactic completions expected
|
|
--^ completion
|
|
skip
|
|
|
|
example : True := by
|
|
exact by
|
|
-- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True := by
|
|
exact by
|
|
-- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True := by
|
|
exact by
|
|
skip
|
|
-- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True := by
|
|
exact by
|
|
skip
|
|
-- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True := by
|
|
exact
|
|
-- No completions expected
|
|
--^ completion
|
|
|
|
example : True := by
|
|
exact
|
|
-- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True :=
|
|
let foo := by
|
|
-- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True :=
|
|
let foo := by
|
|
-- No completions expected
|
|
--^ completion
|
|
|
|
example : True :=
|
|
let foo := by
|
|
skip
|
|
-- All tactic completions expected
|
|
--^ completion
|
|
|
|
example : True :=
|
|
let foo := by
|
|
skip
|
|
-- No completions expected
|
|
--^ completion
|
|
|
|
example : True := by {
|
|
-- All tactic completions expected
|
|
--^ completion
|
|
}
|
|
|
|
example : True := by
|
|
{ skip -- All tactic completions expected
|
|
}
|
|
--^ completion
|
|
|
|
/-!
|
|
Now check that first token detection and tactic names work correctly in completion.
|
|
-/
|
|
|
|
/-- Local def -/
|
|
syntax "let " letDecl : tactic
|
|
|
|
/-- Local recursive def -/
|
|
@[tactic_name "let rec"]
|
|
syntax (name := letrec) "let " &"rec" letRecDecls : tactic
|
|
|
|
example : True := by
|
|
-- All tactic completions expected
|
|
--^ completion
|