feat: better error message for "unknown" tactic

@Kha The hack I posted at Zulip didn't really work
```
macro x:ident : tactic => throw $ Lean.Macro.Exception.error x s!"unknown tactic '{x.getId}'"
```

For example, we would still get a weird error message at
```
theorem ex3 (x : Nat) : x = x → x = x :=
  have x = x by foo (aaa bbb) -- The error would be at `bbb`
  fun h => h
```
There were other minor issues that could be fixed, but this one was bad.

src/Lean/Parser/Basic.lean

@@ -129,7 +129,7 @@ structure ParserContext extends InputContext :=
   (tokens             : TokenTable)
   (insideQuot         : Bool := false)
   (suppressInsideQuot : Bool := false)
-  (savedPos?          : Option Position := none)
+  (savedPos?          : Option String.Pos := none)
   (forbiddenTk?       : Option Token := none)
 
 structure Error :=
@@ -366,6 +366,21 @@ def errorFn (msg : String) : ParserFn := fun _ s =>
   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.input.next pos else pos
+    match s with
+    | ⟨stack, _, cache, _⟩ => ⟨stack, pos, cache, some { unexpected := msg }⟩
+
+/- 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.  -/
+@[inline] def errorAtSavedPos (msg : String) (delta : Bool) : Parser := {
+  fn := errorAtSavedPosFn msg delta
+}
+
 /- Succeeds if `c.prec <= prec` -/
 def checkPrecFn (prec : Nat) : ParserFn := fun c s =>
   if c.prec <= prec then s
@@ -1332,7 +1347,8 @@ def anyOfFn : List Parser → ParserFn
   match c.savedPos? with
   | none => s
   | some savedPos =>
-    let pos := c.fileMap.toPosition s.pos
+    let savedPos := c.fileMap.toPosition savedPos
+    let pos      := c.fileMap.toPosition s.pos
     if pos.column ≥ savedPos.column then s
     else s.mkError errorMsg
 
@@ -1343,7 +1359,8 @@ def anyOfFn : List Parser → ParserFn
   match c.savedPos? with
   | none => s
   | some savedPos =>
-    let pos := c.fileMap.toPosition s.pos
+    let savedPos := c.fileMap.toPosition savedPos
+    let pos      := c.fileMap.toPosition s.pos
     if pos.column > savedPos.column then s
     else s.mkError errorMsg
 
@@ -1354,7 +1371,8 @@ def anyOfFn : List Parser → ParserFn
   match c.savedPos? with
   | none => s
   | some savedPos =>
-    let pos := c.fileMap.toPosition s.pos
+    let savedPos := c.fileMap.toPosition savedPos
+    let pos      := c.fileMap.toPosition s.pos
     if pos.line == savedPos.line then s
     else s.mkError errorMsg
 
@@ -1364,8 +1382,7 @@ def anyOfFn : List Parser → ParserFn
 @[inline] def withPosition (p : Parser) : Parser := {
   info := p.info,
   fn   := fun c s =>
-    let pos := c.fileMap.toPosition s.pos
-    p.fn { c with savedPos? := pos } s
+    p.fn { c with savedPos? := s.pos } s
 }
 
 @[inline] def withoutPosition (p : Parser) : Parser := {

src/Lean/Parser/Tactic.lean

@@ -43,6 +43,7 @@ def ident' : Parser := ident <|> underscore
 @[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
 @[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> tacticSeq
 @[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize " >> optional («try» (ident >> " : ")) >> termParser 51 >> " = " >> ident
+@[builtinTacticParser] def «unknown»    := parser! withPosition (ident >> errorAtSavedPos "unknown tactic" true)
 
 def locationWildcard := parser! "*"
 def locationTarget   := parser! unicodeSymbol "⊢" "|-"

src/Lean/PrettyPrinter/Formatter.lean

@@ -192,6 +192,8 @@ def categoryParserOfStack.formatter (offset : Nat) : Formatter := do
 
 @[combinatorFormatter Lean.Parser.error]
 def error.formatter (msg : String) : Formatter := pure ()
+@[combinatorFormatter Lean.Parser.errorAtSavedPos]
+def errorAtSavedPos.formatter (msg : String) (delta : Bool) : Formatter := pure ()
 @[combinatorFormatter Lean.Parser.try]
 def try.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.lookahead]

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -330,6 +330,10 @@ def level.parenthesizer : CategoryParenthesizer | prec => do
 def error.parenthesizer (msg : String) : Parenthesizer :=
   pure ()
 
+@[combinatorParenthesizer Lean.Parser.errorAtSavedPos]
+def errorAtSavedPos.parenthesizer (msg : String) (delta : Bool) : Parenthesizer :=
+  pure ()
+
 @[combinatorParenthesizer Lean.Parser.try]
 def try.parenthesizer (p : Parenthesizer) : Parenthesizer :=
   p

tests/lean/unknownTactic.lean

@@ -0,0 +1,15 @@
+theorem ex1 (x : Nat) : x = x → x = x := by
+  intro
+  aexact (rfl)
+
+#print "---"
+
+theorem ex2 (x : Nat) : x = x → x = x :=
+  have x = x by foo
+  fun h => h
+
+#print "---"
+
+theorem ex3 (x : Nat) : x = x → x = x :=
+  have x = x by foo (aaa bbb)
+  fun h => h

tests/lean/unknownTactic.lean.expected.out

@@ -0,0 +1,5 @@
+unknownTactic.lean:3:3: error: unknown tactic
+---
+unknownTactic.lean:8:17: error: unknown tactic
+---
+unknownTactic.lean:14:17: error: unknown tactic