From 05c6e1461e791e6b5f10e9f5679dc7df57f55b28 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Sep 2014 09:47:19 -0700
Subject: [PATCH] fix(tests/lean/interactive): interactive tests expected
 output, they must include the new '-- BEGINWAIT' messages

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/interactive/in1.input.expected.out | 12 ++++++++++++
 tests/lean/interactive/in2.input.expected.out |  2 ++
 tests/lean/interactive/in4.input.expected.out |  4 ++++
 tests/lean/interactive/in5.input.expected.out |  2 ++
 tests/lean/interactive/t4.input.expected.out  |  2 ++
 5 files changed, 22 insertions(+)

diff --git a/tests/lean/interactive/in1.input.expected.out b/tests/lean/interactive/in1.input.expected.out
index 25318909a..4c3f228c2 100644
--- a/tests/lean/interactive/in1.input.expected.out
+++ b/tests/lean/interactive/in1.input.expected.out
@@ -1,3 +1,5 @@
+-- BEGINWAIT
+-- ENDWAIT
 -- BEGININFO
 -- SYMBOL|4|22
 Type
@@ -21,6 +23,8 @@ A
 a
 -- ACK
 -- ENDINFO
+-- BEGINWAIT
+-- ENDWAIT
 -- BEGININFO
 -- SYMBOL|4|22
 Type
@@ -44,6 +48,8 @@ B
 b
 -- ACK
 -- ENDINFO
+-- BEGINWAIT
+-- ENDWAIT
 -- BEGININFO
 -- SYMBOL|5|22
 Type
@@ -67,6 +73,8 @@ B
 b
 -- ACK
 -- ENDINFO
+-- BEGINWAIT
+-- ENDWAIT
 -- BEGININFO
 -- SYMBOL|4|22
 Type
@@ -90,6 +98,10 @@ B
 b
 -- ACK
 -- ENDINFO
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINWAIT
+-- ENDWAIT
 -- BEGININFO
 -- SYMBOL|4|22
 Type
diff --git a/tests/lean/interactive/in2.input.expected.out b/tests/lean/interactive/in2.input.expected.out
index 36c751f4c..9d4e747c9 100644
--- a/tests/lean/interactive/in2.input.expected.out
+++ b/tests/lean/interactive/in2.input.expected.out
@@ -6,6 +6,8 @@ Type : Type
 -- BEGINEVAL
 Type.{1} : Type.{2}
 -- ENDEVAL
+-- BEGINWAIT
+-- ENDWAIT
 -- BEGINEVAL
 tst.foo.{l_1 l_2} : ?M_1 → ?M_2 → ?M_1
 -- ENDEVAL
diff --git a/tests/lean/interactive/in4.input.expected.out b/tests/lean/interactive/in4.input.expected.out
index 336d7eefa..13d321580 100644
--- a/tests/lean/interactive/in4.input.expected.out
+++ b/tests/lean/interactive/in4.input.expected.out
@@ -1,3 +1,5 @@
+-- BEGINWAIT
+-- ENDWAIT
 -- BEGININFO
 -- TYPE|9|0
 eq (tst.foo a b) (tst.foo a b)
@@ -11,6 +13,8 @@ rfl
 -- ENDINFO
 -- BEGININFO NAY
 -- ENDINFO
+-- BEGINWAIT
+-- ENDWAIT
 -- BEGININFO
 -- TYPE|9|0
 eq (tst.foo a b) (tst.foo a b)
diff --git a/tests/lean/interactive/in5.input.expected.out b/tests/lean/interactive/in5.input.expected.out
index 025467f6f..548b8df39 100644
--- a/tests/lean/interactive/in5.input.expected.out
+++ b/tests/lean/interactive/in5.input.expected.out
@@ -1,3 +1,5 @@
+-- BEGINWAIT
+-- ENDWAIT
 -- BEGININFO
 -- TYPE|4|0
 A → B → and A B
diff --git a/tests/lean/interactive/t4.input.expected.out b/tests/lean/interactive/t4.input.expected.out
index 1eda2f5af..97a8dcbb9 100644
--- a/tests/lean/interactive/t4.input.expected.out
+++ b/tests/lean/interactive/t4.input.expected.out
@@ -1,3 +1,5 @@
+-- BEGINWAIT
+-- ENDWAIT
 -- BEGININFO
 -- TYPE|6|6
 (nat → Prop) → nat