Optional delaborators

Stream: lean4

[Eric Wieser]

For debugging, it would have been helpful to me to have this delaborator:

/-- Delaborator for `no_index`. -/
@[delab mdata]
def delabNoIndex : Delab := do
  let .mdata d e ← SubExpr.getExpr | failure
  let .some (.ofBool .true) := d.find `noindex | failure
  let d := d.erase `noindex
  let inner ← withReader (fun s => {s with subExpr.expr := .mdata d e}) delab
  `(no_index $inner)

Having this enabled by default would certainly be confusing; Is the appropriate thing to do here to hide this behind a new pp option, or make the delaborator attribute scoped?