fix: goal state on conv =>

src/Init/Conv.lean

@@ -14,7 +14,9 @@ declare_syntax_cat conv (behavior := both)
 
 syntax convSeq1Indented := withPosition((group(colGe conv ";"?))+)
 syntax convSeqBracketed := "{" (group(conv ";"?))+ "}"
-syntax convSeq := convSeq1Indented <|> convSeqBracketed
+-- Order is important: a missing `conv` proof should not be parsed as `{ <missing> }`,
+-- automatically closing goals
+syntax convSeq := convSeqBracketed <|> convSeq1Indented
 
 syntax (name := conv) "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic
 

src/Lean/Elab/Tactic/Conv/Basic.lean

@@ -131,7 +131,7 @@ def remarkAsConvGoal : TacticM Unit := do
 
 private def convTarget (conv : Syntax) : TacticM Unit := withMainContext do
    let target ← getMainTarget
-   let (targetNew, proof) ← convert target (evalTactic conv)
+   let (targetNew, proof) ← convert target (withTacticInfoContext (← getRef) (evalTactic conv))
    liftMetaTactic1 fun mvarId => replaceTargetEq mvarId targetNew proof
    evalTactic (← `(tactic| try rfl))
 

tests/lean/interactive/plainGoal.lean

@@ -88,11 +88,16 @@ example : True := (by exact True.intro)
 example : True := (by exact True.intro )
                                      --^ $/lean/plainGoal
 
-set_option trace.Elab.info true
 example : True ∧ False := by
   · constructor; constructor
               --^ $/lean/plainGoal
 
+example : True = True := by
+  conv =>
+      --^ $/lean/plainGoal
+    --
+  --^ $/lean/plainGoal
+
 example : False := by
 -- EOF test
 --^ $/lean/plainGoal

tests/lean/interactive/plainGoal.lean.expected.out

@@ -114,10 +114,16 @@
  "position": {"line": 87, "character": 39}}
 null
 {"textDocument": {"uri": "file://plainGoal.lean"},
- "position": {"line": 92, "character": 16}}
+ "position": {"line": 91, "character": 16}}
 {"rendered":
  "```lean\ncase left\n⊢ True\n```\n---\n```lean\ncase right\n⊢ False\n```",
  "goals": ["case left\n⊢ True", "case right\n⊢ False"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
- "position": {"line": 96, "character": 2}}
+ "position": {"line": 95, "character": 8}}
+{"rendered": "```lean\n| True = True\n```", "goals": ["| True = True"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 97, "character": 4}}
+{"rendered": "```lean\n| True = True\n```", "goals": ["| True = True"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 101, "character": 2}}
 {"rendered": "```lean\n⊢ False\n```", "goals": ["⊢ False"]}