From db6b9db07ed630ecb13fac7c864e252f132afe75 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 15 Oct 2018 12:47:32 +0200 Subject: [PATCH] fix(tests/lean/parser1): fix reprinting (`eoi node was missing) --- tests/lean/parser1.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean index d46282a3eb..431e68c862 100644 --- a/tests/lean/parser1.lean +++ b/tests/lean/parser1.lean @@ -115,7 +115,7 @@ def run_frontend (input : string) : except_t string io unit := do when ¬(cmd'.is_of_kind module.eoi) $ io.println "elaborator died!!", msgs.to_list.mfor $ λ e, io.println e.text, - pure (sum.inr outs.reverse) + pure $ sum.inr (out::outs).reverse } | coroutine_result_core.yielded elab_out elab_k := do { elab_out.messages.to_list.mfor $ λ e, io.println e.text, @@ -126,7 +126,7 @@ def run_frontend (input : string) : except_t string io unit := do }, check_reprint outs input/-, let stx := syntax.node ⟨none, outs.map (λ r, r.cmd)⟩, - let stx := stx.update_leading s, + let stx := stx.update_leading input, io.println "result:", io.println (to_string stx)-/ #exit