feat: grind_pattern for Subtype.property

src/Init/Prelude.lean

@@ -631,6 +631,8 @@ structure Subtype {α : Sort u} (p : α → Prop) where
   -/
   property : p val
 
+grind_pattern Subtype.property => self.val
+
 set_option linter.unusedVariables.funArgs false in
 /--
 Gadget for optional parameter support.

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -250,6 +250,9 @@ 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,6 +142,19 @@ 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,6 +20,15 @@ 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,6 +319,8 @@ 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,6 +410,10 @@ 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

tests/lean/interactive/completionTactics.lean.expected.out

@@ -32,6 +32,9 @@
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -77,6 +80,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -92,7 +99,100 @@ Resolution of Lean.Parser.Tactic.introMatch:
  "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 26, "character": 24}}
-{"items": [], "isIncomplete": true}
+{"items":
+ [{"label": "Lean.Parser.Tactic.open",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
+    "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
+  {"label": "Lean.Parser.Tactic.match",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
+    "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
+  {"label": "Lean.Parser.Tactic.set_option",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,\nbut it sets the option only within the tactics `tacs`. ",
+    "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
+  {"label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
+  {"label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
+  {"label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
+  {"label": "Lean.Parser.Tactic.introMatch",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
+    "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}],
+ "isIncomplete": false}
+Resolution of Lean.Parser.Tactic.open:
+{"label": "Lean.Parser.Tactic.open",
+ "kind": 14,
+ "documentation":
+ {"value":
+  "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
+  "kind": "markdown"},
+ "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
+Resolution of Lean.Parser.Tactic.match:
+{"label": "Lean.Parser.Tactic.match",
+ "kind": 14,
+ "documentation":
+ {"value":
+  "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
+  "kind": "markdown"},
+ "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
+Resolution of Lean.Parser.Tactic.set_option:
+{"label": "Lean.Parser.Tactic.set_option",
+ "kind": 14,
+ "documentation":
+ {"value":
+  "`set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,\nbut it sets the option only within the tactics `tacs`. ",
+  "kind": "markdown"},
+ "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
+Resolution of skip:
+{"label": "skip",
+ "kind": 14,
+ "documentation": {"value": "A docstring ", "kind": "markdown"},
+ "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
+Resolution of Lean.Parser.Tactic.nestedTactic:
+{"label": "Lean.Parser.Tactic.nestedTactic",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
+Resolution of exact:
+{"label": "exact",
+ "kind": 14,
+ "documentation": {"value": "Another docstring ", "kind": "markdown"},
+ "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
+Resolution of Lean.Parser.Tactic.introMatch:
+{"label": "Lean.Parser.Tactic.introMatch",
+ "kind": 14,
+ "documentation":
+ {"value":
+  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
+  "kind": "markdown"},
+ "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 29, "character": 25}}
 {"items": [], "isIncomplete": true}
@@ -127,6 +227,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -172,6 +275,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -216,6 +323,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -261,6 +371,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -305,6 +419,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -350,6 +467,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -394,6 +515,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -439,6 +563,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -483,6 +611,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -528,6 +659,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -572,6 +707,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -617,6 +755,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -661,6 +803,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -706,6 +851,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -750,6 +899,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -795,6 +947,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -839,6 +995,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -884,6 +1043,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -928,6 +1091,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -973,6 +1139,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -1020,6 +1190,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -1065,6 +1238,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -1109,6 +1286,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -1154,6 +1334,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -1198,6 +1382,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -1243,6 +1430,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -1287,6 +1478,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -1332,6 +1526,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -1379,6 +1577,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -1424,6 +1625,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,
@@ -1468,6 +1673,9 @@ Resolution of Lean.Parser.Tactic.introMatch:
   {"label": "Lean.Parser.Tactic.nestedTactic",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]},
+  {"label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
@@ -1513,6 +1721,10 @@ Resolution of Lean.Parser.Tactic.nestedTactic:
 {"label": "Lean.Parser.Tactic.nestedTactic",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}
+Resolution of Lean.Parser.Tactic.unknown:
+{"label": "Lean.Parser.Tactic.unknown",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}
 Resolution of exact:
 {"label": "exact",
  "kind": 14,

tests/lean/unknownTactic.lean.expected.out

@@ -1,15 +1,15 @@
-unknownTactic.lean:1:41-2:7: error: unsolved goals
+unknownTactic.lean:3:3: error: unknown tactic
+unknownTactic.lean:1:41-3:8: error: unsolved goals
 x : Nat
 a✝ : x = x
 ⊢ x = x
-unknownTactic.lean:3:2-3:8: error: unexpected identifier; expected command
 ---
-unknownTactic.lean:8:20-8:24: error: unexpected identifier; expected '{' or tactic
-unknownTactic.lean:8:18-8:20: error: unsolved goals
+unknownTactic.lean:8:22: error: unknown tactic
+unknownTactic.lean:8:18-8:24: error: unsolved goals
 x : Nat
 ⊢ x = x
 ---
-unknownTactic.lean:14:20-14:24: error: unexpected identifier; expected '{' or tactic
-unknownTactic.lean:14:18-14:20: error: unsolved goals
+unknownTactic.lean:14:22: error: unknown tactic
+unknownTactic.lean:14:18-14:24: error: unsolved goals
 x : Nat
 ⊢ x = x