feat: optionally add information to all symbols during delaboration

Add an option called pp.tagSymbols which, if set, makes the
delaborator add term information to all symbols it can during
delaboration. This option is disabled per default because it would
break the LSP server's hovering behaviour. It is however useful
when for example automatically generating interactive documentation.

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -100,11 +100,17 @@ def delabConst : Delab := do
           c := `_root_ ++ c
         else
           c := c₀
-      return mkIdent c
+      mkIdent c
     else
       `($(mkIdent c).{$[$(ls.toArray.map quote)],*})
 
-  maybeAddBlockImplicit stx
+  let stx ← maybeAddBlockImplicit stx
+  if (←getPPOption getPPTagSymbols) then
+    let stx ← annotateCurPos stx
+    addTermInfo (←getPos) stx (←getExpr)
+    stx
+  else
+    stx
 
 structure ParamKind where
   name        : Name

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -90,6 +90,11 @@ register_builtin_option pp.safeShadowing  : Bool := {
   group    := "pp"
   descr    := "(pretty printer) allow variable shadowing if there is no collision"
 }
+register_builtin_option pp.tagSymbols : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) tag symbol syntax with information"
+}
 register_builtin_option pp.proofs : Bool := {
   defValue := false
   group    := "pp"
@@ -180,6 +185,7 @@ def getPPMatch (o : Options) : Bool := o.get pp.match.name (!getPPAll o)
 def getPPStructureProjections (o : Options) : Bool := o.get pp.structureProjections.name (!getPPAll o)
 def getPPStructureInstances (o : Options) : Bool := o.get pp.structureInstances.name (!getPPAll o)
 def getPPStructureInstanceType (o : Options) : Bool := o.get pp.structureInstanceTypes.name (getPPAll o)
+def getPPTagSymbols (o : Options) : Bool := o.get pp.tagSymbols.name (getPPAll o)
 def getPPUniverses (o : Options) : Bool := o.get pp.universes.name (getPPAll o)
 def getPPFullNames (o : Options) : Bool := o.get pp.fullNames.name (getPPAll o)
 def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPAll o)