max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: explicit structure for PPExprTaggedRequest

Browse source
This commit is contained in:
E.W.Ayers 2022-06-10 13:01:39 -04:00 • committed by Leonardo de Moura
parent 69facfbe8e
commit fd66e70d1e
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Server/FileWorker/WidgetRequests.lean
View file

@ -17,12 +17,17 @@ import Lean.Server.FileWorker.RequestHandling
namespace Lean.Widget
open Server
structure PPExprTaggedRequest where
expr : WithRpcRef ExprWithCtx
explicit : Bool
deriving Inhabited, RpcEncoding
builtin_initialize
registerBuiltinRpcProcedure
`Lean.Widget.ppExprTagged
(WithRpcRef ExprWithCtx × Bool)
PPExprTaggedRequest
CodeWithInfos
fun (⟨ctx, lctx, expr⟩, explicit) => RequestM.asTask do
fun ⟨⟨ctx, lctx, expr⟩, explicit⟩ => RequestM.asTask do
ctx.runMetaM lctx do
ppExprTagged expr explicit