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

@@ -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

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,

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);

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

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"}}