From e39eebabd93262e65d1fc44f6b904e84e23280b5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 1 Aug 2022 13:01:37 -0700 Subject: [PATCH] fix: move doc string to parser that sets the `SyntaxNodeKind` for the `{ tac }` notation see #1403 This fixes the hover for `{ tac }` --- src/Lean/Parser/Tactic.lean | 2 -- src/Lean/Parser/Term.lean | 2 ++ 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index f78fad7b9f..a68648cdfe 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -20,8 +20,6 @@ example : True := by foo -- unknown tactic -/ @[builtinTacticParser] def «unknown» := leading_parser withPosition (ident >> errorAtSavedPos "unknown tactic" true) -/-- The syntax `{ tacs }` is an alternative syntax for `· tacs`. -It runs the tactics in sequence, and fails if the goal is not solved. -/ @[builtinTacticParser] def nestedTactic := tacticSeqBracketed def matchRhs := Term.hole <|> Term.syntheticHole <|> tacticSeq diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 4c48c4d182..95a4f753cf 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -33,6 +33,8 @@ namespace Tactic def tacticSeq1Indented : Parser := leading_parser many1Indent (group (ppLine >> tacticParser >> optional ";")) +/-- The syntax `{ tacs }` is an alternative syntax for `· tacs`. +It runs the tactics in sequence, and fails if the goal is not solved. -/ def tacticSeqBracketed : Parser := leading_parser "{" >> many (group (ppLine >> tacticParser >> optional ";")) >> ppDedent (ppLine >> "}") def tacticSeq :=