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

fix: position info for rw tactics of the form rw [h1, h2, ..]

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-08 18:18:37 -08:00
parent 90cab68332
commit 23319da6c0
1 changed files with 14 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Lean/Elab/Tactic/Rewrite.lean
View file

@ -11,15 +11,23 @@ import Lean.Elab.Tactic.Location
namespace Lean.Elab.Tactic
open Meta
private def expand (kind : SyntaxNodeKind) (token : String) (stx : Syntax) : Syntax := do
let rwRules := stx[1][1].getSepArgs
let loc := stx[2]
let mut newTacs := #[]
for i in [:rwRules.size] do
let rwRule := rwRules[i]
-- We use `stx` as "position provider" for the first rule
-- Without this change, we don't get correct information when we hover over `rw`/`rewrite`/`erewrite` with multiple rewrites
let ref ← if i == 0 then stx else pure rwRule
newTacs := newTacs.push <| Syntax.node kind #[mkAtomFrom ref token, rwRule, loc]
return mkNullNode newTacs
@[builtinMacro Lean.Parser.Tactic.rewriteSeq] def expandRewriteTactic : Macro := fun stx =>
let seq := stx[1][1].getSepArgs
let loc := stx[2]
return mkNullNode <| seq.map fun rwRule => Syntax.node ``Parser.Tactic.rewrite #[mkAtomFrom rwRule "rewrite ", rwRule, loc]
return expand ``Parser.Tactic.rewrite "rewrite " stx
@[builtinMacro Lean.Parser.Tactic.erewriteSeq] def expandERewriteTactic : Macro := fun stx =>
let seq := stx[1][1].getSepArgs
let loc := stx[2]
return mkNullNode <| seq.map fun rwRule => Syntax.node ``Parser.Tactic.erewrite #[mkAtomFrom rwRule "erewrite ", rwRule, loc]
return expand ``Parser.Tactic.erewrite "erewrite " stx
def rewriteTarget (stx : Syntax) (symm : Bool) (mode : TransparencyMode) : TacticM Unit := do
let (g, gs) ← getMainGoal