diff --git a/tests/lean/run/Reformat.lean b/tests/lean/run/Reformat.lean index 54cec70577..21efe78f85 100644 --- a/tests/lean/run/Reformat.lean +++ b/tests/lean/run/Reformat.lean @@ -14,7 +14,7 @@ let (debug, f) : Bool × String := match args with table ← Parser.builtinTokenTable.get; env ← mkEmptyEnvironment; stx ← Lean.Parser.parseFile env args.head!; -(f, _) ← IO.runMeta (PrettyPrinter.ppModule table stx) env { opts := KVMap.insert {} `trace.PrettyPrinter.format debug }; +f ← (PrettyPrinter.ppModule table stx).toIO env (KVMap.insert {} `trace.PrettyPrinter.format debug); IO.print f; let inputCtx := Parser.mkInputContext (toString f) ""; let (stx', state, messages) := Parser.parseHeader env inputCtx; diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean index abfe0ccff4..c47524b7b2 100644 --- a/tests/lean/run/Reparen.lean +++ b/tests/lean/run/Reparen.lean @@ -30,8 +30,8 @@ IO.print s; let cmds := stx.getArgs.extract 1 stx.getArgs.size; cmds.forM $ fun cmd => do let cmd := unparen cmd; - (cmd, _) ← IO.runMeta (PrettyPrinter.parenthesizeCommand cmd) - env { opts := KVMap.insert {} `trace.PrettyPrinter.parenthesize debug }; + cmd ← (PrettyPrinter.parenthesizeCommand cmd).toIO + env (KVMap.insert {} `trace.PrettyPrinter.parenthesize debug); some s ← pure cmd.reprint | throw $ IO.userError "cmd reprint failed"; IO.print s @@ -50,4 +50,3 @@ open Lean syntax:80 term " ^~ " term:80 : term syntax:70 term " *~ " term:71 : term #eval check $ Unhygienic.run `(((1 + 2) *~ 3) ^~ 4) -