test: Reformat.lean: make output test

This commit is contained in:
Sebastian Ullrich 2020-10-08 15:52:27 +02:00
parent 6eaba0dc6f
commit 549912bbf4
3 changed files with 2232 additions and 2 deletions

View file

@ -3,7 +3,7 @@ open Lean
open Lean.Format
def eval (w : Nat) (f : Format) : IO Unit := do
IO.println $ be w 0 "" [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent := 0 }] }]
IO.println $ f.prettyAux w
-- hard line breaks should re-evaluate flattening behavior within group
#eval eval 5 $ group (text "a" ++ line ++ text "b\nlooooooooong" ++ line ++ text "c") ++ line ++ text "d"

View file

@ -23,4 +23,4 @@ if stx' != stx then
if stx.getArg i != stx'.getArg i then
throw $ IO.userError s!"reparsing failed:\n{stx.getArg i}\n{stx'.getArg i}"
#eval main ["../../../src/Init/Core.lean"]
#eval main ["../../src/Init/Core.lean"]

File diff suppressed because it is too large Load diff