From e5d44f40332b798ea9cbd895a5f2c8f2941fb226 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 21 Aug 2024 22:47:19 +0200 Subject: [PATCH] fix: hover text over `_` in `?_` (#5118) in principle we'd like to use the existing parser ``` "?" >> (ident <|> hole) ``` but somehow annotate it so that hovering the `hole` will not show the hole's hover. But for now it was easier to just change the parser to ``` "?" >> (ident <|> "_") ``` and be done with it. Fixes #5021 --- src/Lean/Elab/Term.lean | 6 +--- src/Lean/Parser/Term.lean | 2 +- stage0/src/stdlib_flags.h | 2 +- tests/lean/interactive/issue5021.lean | 11 +++++++ .../interactive/issue5021.lean.expected.out | 32 +++++++++++++++++++ 5 files changed, 46 insertions(+), 7 deletions(-) create mode 100644 tests/lean/interactive/issue5021.lean create mode 100644 tests/lean/interactive/issue5021.lean.expected.out diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index ea14af6e70..b67cb64f7c 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1308,11 +1308,7 @@ private partial def dropTermParens : Syntax → Syntax := fun stx => | _ => stx private def isHole (stx : Syntax) : Bool := - match stx with - | `(_) => true - | `(? _) => true - | `(? $_:ident) => true - | _ => false + stx.isOfKind ``Lean.Parser.Term.hole || stx.isOfKind ``Lean.Parser.Term.syntheticHole private def isTacticBlock (stx : Syntax) : Bool := match stx with diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 0598cb401f..66a0ba3556 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -145,7 +145,7 @@ def optSemicolon (p : Parser) : Parser := /-- Parses a "synthetic hole", that is, `?foo` or `?_`. This syntax is used to construct named metavariables. -/ @[builtin_term_parser] def syntheticHole := leading_parser - "?" >> (ident <|> hole) + "?" >> (ident <|> "_") /-- The `⋯` term denotes a term that was omitted by the pretty printer. The presence of `⋯` in pretty printer output is controlled by the `pp.deepTerms` and `pp.proofs` options, diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 0699845ba4..658ab0874e 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -8,7 +8,7 @@ options get_default_options() { // switch to `true` for ABI-breaking changes affecting meta code opts = opts.update({"interpreter", "prefer_native"}, false); // switch to `true` for changing built-in parsers used in quotations - opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); + opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true); // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax // with custom precheck hooks were affected opts = opts.update({"quotPrecheck"}, true); diff --git a/tests/lean/interactive/issue5021.lean b/tests/lean/interactive/issue5021.lean new file mode 100644 index 0000000000..d4d1b1b7d2 --- /dev/null +++ b/tests/lean/interactive/issue5021.lean @@ -0,0 +1,11 @@ +example : False := by + refine ?_ + --^ textDocument/hover + --^ textDocument/hover + sorry + +example : False := by + refine ? _ -- check that a space is allowed + --^ textDocument/hover + --^ textDocument/hover + sorry diff --git a/tests/lean/interactive/issue5021.lean.expected.out b/tests/lean/interactive/issue5021.lean.expected.out new file mode 100644 index 0000000000..e4179d64a8 --- /dev/null +++ b/tests/lean/interactive/issue5021.lean.expected.out @@ -0,0 +1,32 @@ +{"textDocument": {"uri": "file:///issue5021.lean"}, + "position": {"line": 1, "character": 9}} +{"range": + {"start": {"line": 1, "character": 9}, "end": {"line": 1, "character": 11}}, + "contents": + {"value": + "```lean\nFalse\n```\n***\nParses a \"synthetic hole\", that is, `?foo` or `?_`.\nThis syntax is used to construct named metavariables. ", + "kind": "markdown"}} +{"textDocument": {"uri": "file:///issue5021.lean"}, + "position": {"line": 1, "character": 10}} +{"range": + {"start": {"line": 1, "character": 9}, "end": {"line": 1, "character": 11}}, + "contents": + {"value": + "```lean\nFalse\n```\n***\nParses a \"synthetic hole\", that is, `?foo` or `?_`.\nThis syntax is used to construct named metavariables. ", + "kind": "markdown"}} +{"textDocument": {"uri": "file:///issue5021.lean"}, + "position": {"line": 7, "character": 9}} +{"range": + {"start": {"line": 7, "character": 9}, "end": {"line": 7, "character": 12}}, + "contents": + {"value": + "```lean\nFalse\n```\n***\nParses a \"synthetic hole\", that is, `?foo` or `?_`.\nThis syntax is used to construct named metavariables. ", + "kind": "markdown"}} +{"textDocument": {"uri": "file:///issue5021.lean"}, + "position": {"line": 7, "character": 11}} +{"range": + {"start": {"line": 7, "character": 9}, "end": {"line": 7, "character": 12}}, + "contents": + {"value": + "```lean\nFalse\n```\n***\nParses a \"synthetic hole\", that is, `?foo` or `?_`.\nThis syntax is used to construct named metavariables. ", + "kind": "markdown"}}