From 1f6abcaf6cfa3b1fa249a8120901b9e51b6fd816 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 2 Feb 2025 15:29:12 -0800 Subject: [PATCH] feat: make all app unexpanders respond to `pp.tagAppFns` (#6730) This PR changes how app unexpanders are invoked. Before the ref was `.missing`, but now the ref is the head constant's delaborated syntax. This way, when `pp.tagAppFns` is true, then tokens in app unexpanders are annotated with the head constant. The consequence is that in docgen, tokens will be linkified. This new behavior is consistent with how `notation` defines app unexpanders. In a followup PR we can slightly simplify the `notation` unexpander macro to not set the ref. --- .../PrettyPrinter/Delaborator/Builtins.lean | 20 ++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 87a7d4f01199..44a435655a32 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -464,15 +464,21 @@ where /-- Runs the given unexpanders, returning the resulting syntax if any are applicable, and otherwise fails. -/ - tryUnexpand (fs : List Unexpander) (stx : Syntax) : DelabM Syntax := do - fs.firstM fun f => - match f stx |>.run .missing |>.run () with + tryUnexpand (ref : Syntax) (fs : List Unexpander) (stx : Syntax) : DelabM Syntax := do + withAnnotateTermInfoUnlessAnnotated <| fs.firstM fun f => + match f stx |>.run ref |>.run () with | EStateM.Result.ok stx _ => return stx | _ => failure /-- If the expression is a candidate for app unexpanders, try applying an app unexpander using some prefix of the arguments, longest prefix first. This function makes sure that the unexpanded syntax is annotated and given TermInfo so that it is hoverable in the InfoView. + + Ref logic: + 1. The unexpanders are run with the head constant's syntax as the ref. + 2. If `pp.tagAppFns` is false, then this does nothing, since `delabConst` won't register any terminfo for the constant. + 3. If `pp.tagAppFns` is true, then this causes all tokens in app unexpanders to refer to the head constant. + The effect is that in docgen, every token will be linkified (supposing the app unexpander uses syntax quotations). -/ tryAppUnexpanders (fnStx : Term) (args : Array AppImplicitArg) : Delab := do let .const c _ := (← getExpr).getAppFn.consumeMData | unreachable! @@ -481,13 +487,13 @@ where let rec go (i : Nat) (implicitArgs : Nat) (argStxs : Array Syntax) : DelabM Term := do match i with | 0 => - let stx ← tryUnexpand fs fnStx - return Syntax.mkApp (← annotateTermInfo stx) (args.filterMap (·.syntax?)) + let stx ← tryUnexpand fnStx fs fnStx + return Syntax.mkApp stx (args.filterMap (·.syntax?)) | i' + 1 => if args[i']!.syntax?.isSome then - (do let stx ← tryUnexpand fs <| Syntax.mkApp fnStx argStxs + (do let stx ← tryUnexpand fnStx fs <| Syntax.mkApp fnStx argStxs let argStxs' := args.extract i args.size |>.filterMap (·.syntax?) - return Syntax.mkApp (← annotateTermInfo stx) argStxs') + return Syntax.mkApp stx argStxs') <|> withBoundedAppFn (implicitArgs + 1) (go i' 0 argStxs.pop) else go i' (implicitArgs + 1) argStxs