From 742d053a97bdd109a41a921facd1cd6a55e89bc7 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 30 Mar 2023 16:16:19 -0700
Subject: [PATCH] fix: respect pp.raw in interactive .ofGoal

Fixes #2175
---
 src/Lean/Widget/InteractiveCode.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index edff58cfd5..280ea1e53b 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -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