fix: respect pp.raw in interactive .ofGoal

Fixes #2175
This commit is contained in:
Gabriel Ebner 2023-03-30 16:16:19 -07:00
parent 39f0fa670a
commit 742d053a97

View file

@ -74,6 +74,8 @@ where
TaggedText.tag t (go subTt)
def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do
if pp.raw.get (← getOptions) then
return .text (toString e)
let delab := open PrettyPrinter.Delaborator in
if explicit then
withOptionAtCurrPos pp.tagAppFns.name true do