fix: implement · tacs as a builtin elaborator, part 2

Fixes #2153

src/Init/NotationExtra.lean

@@ -372,14 +372,9 @@ macro_rules
     `($mods:declModifiers class $id $params* extends $parents,* $[: $ty]?
       attribute [instance] $ctor)
 
-section
-open Lean.Parser.Tactic
 syntax cdotTk := patternIgnore("· " <|> ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
-macro_rules
-  | `(tactic| $cdot:cdotTk $tacs) => `(tactic| {%$cdot ($tacs) }%$cdot)
-end
 
 /--
   Similar to `first`, but succeeds only if one the given tactics solves the current goal.

src/Lean/Elab/BuiltinTerm.lean

@@ -157,7 +157,7 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
 @[builtin_term_elab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? =>
   elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?)
 
-@[builtin_term_elab cdot] def elabBadCDot : TermElab := fun _ _ =>
+@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun _ _ =>
   throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)"
 
 @[builtin_term_elab str] def elabStrLit : TermElab := fun stx _ => do

tests/lean/interactive/plainGoal.lean

@@ -134,4 +134,3 @@ example : True ∧ False := by
   · --
  --^ $/lean/plainGoal
   --^ $/lean/plainGoal
-  -- TODO: ^

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

@@ -169,5 +169,4 @@ null
 {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 133, "character": 4}}
-{"rendered": "```lean\ncase right\n⊢ False\n```",
- "goals": ["case right\n⊢ False"]}
+{"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}