test: change behavior of unknown tactic parsing

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -250,9 +250,6 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
 
 @[builtin_tactic skip] def evalSkip : Tactic := fun _ => pure ()
 
-@[builtin_tactic unknown] def evalUnknown : Tactic := fun stx => do
-  addCompletionInfo <| CompletionInfo.tactic stx
-
 @[builtin_tactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx =>
   Term.withoutErrToSorry <| withoutRecover do
     let tactic := stx[1]

src/Lean/Parser/Basic.lean

@@ -142,19 +142,6 @@ def error (msg : String) : Parser := {
   fn   := errorFn msg
 }
 
-def errorAtSavedPosFn (msg : String) (delta : Bool) : ParserFn := fun c s =>
-  match c.savedPos? with
-  | none     => s
-  | some pos =>
-    let pos := if delta then c.next pos else pos
-    s.mkUnexpectedErrorAt msg pos
-
-/-- Generate an error at the position saved with the `withPosition` combinator.
-   If `delta == true`, then it reports at saved position+1.
-   This useful to make sure a parser consumed at least one character.  -/
-@[builtin_doc] def errorAtSavedPos (msg : String) (delta : Bool) : Parser := {
-  fn := errorAtSavedPosFn msg delta
-}
 
 /-- Succeeds if `c.prec <= prec` -/
 def checkPrecFn (prec : Nat) : ParserFn := fun c s =>

src/Lean/Parser/Tactic.lean

@@ -20,15 +20,6 @@ builtin_initialize
   register_parser_alias tacticSeq
   register_parser_alias tacticSeqIndentGt
 
-/- This is a fallback tactic parser for any identifier which exists only
-to improve syntax error messages.
-```
-example : True := by foo -- unknown tactic
-```
--/
-@[builtin_tactic_parser] def «unknown»    := leading_parser
-  withPosition (ident >> errorAtSavedPos "unknown tactic" true)
-
 @[builtin_tactic_parser] def nestedTactic := tacticSeqBracketed
 
 def matchRhs  := Term.hole <|> Term.syntheticHole <|> tacticSeq

src/Lean/PrettyPrinter/Formatter.lean

@@ -319,8 +319,6 @@ def parserOfStack.formatter (offset : Nat) (_prec : Nat := 0) : Formatter := do
 
 @[combinator_formatter error, expose]
 def error.formatter (_msg : String) : Formatter := pure ()
-@[combinator_formatter errorAtSavedPos, expose]
-def errorAtSavedPos.formatter (_msg : String) (_delta : Bool) : Formatter := pure ()
 @[combinator_formatter lookahead, expose]
 def lookahead.formatter (_ : Formatter) : Formatter := pure ()
 

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -410,10 +410,6 @@ def rawStx.parenthesizer : CategoryParenthesizer | _ => do
 def error.parenthesizer (_msg : String) : Parenthesizer :=
   pure ()
 
-@[combinator_parenthesizer errorAtSavedPos, expose]
-def errorAtSavedPos.parenthesizer (_msg : String) (_delta : Bool) : Parenthesizer :=
-  pure ()
-
 @[combinator_parenthesizer atomic, expose]
 def atomic.parenthesizer (p : Parenthesizer) : Parenthesizer :=
   p