From 092e26179bfb19790a63e5b9a260b089b1a286b3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 28 Nov 2022 15:47:17 +0100 Subject: [PATCH] chore: fix script/reformat.lean --- script/reformat.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/script/reformat.lean b/script/reformat.lean index 54cf2b7e52..635443bfbb 100644 --- a/script/reformat.lean +++ b/script/reformat.lean @@ -17,7 +17,7 @@ partial def reprintCore : Syntax → Option Format | Syntax.missing => none | Syntax.atom _ val => val.trim | Syntax.ident _ rawVal _ _ => rawVal.toString - | Syntax.node _ kind args => + | Syntax.node _ _ args => match args.toList.filterMap reprintCore with | [] => none | [arg] => arg @@ -29,7 +29,7 @@ def reprint (stx : Syntax) : Format := def printCommands (cmds : Syntax) : CoreM Unit := do for cmd in getCommands cmds |>.run #[] |>.2 do try - IO.println (← ppCommand cmd).pretty + IO.println (← ppCommand ⟨cmd⟩).pretty catch e => IO.println f!"/-\ncannot print: {← e.toMessageData.format}\n{reprint cmd}\n-/" @@ -70,4 +70,4 @@ unsafe def main (args : List String) : IO Unit := do let mut first := true for {env, currNamespace, openDecls, ..} in moduleStx, stx in leadingUpdated do if first then first := false else IO.print "\n" - let _ ← printCommands stx |>.toIO {currNamespace, openDecls} {env} + let _ ← printCommands stx |>.toIO {fileName, fileMap := FileMap.ofString input, currNamespace, openDecls} {env}