[ #4647 ] fixed tests

These interaction tests now produce the expected results (fruits of fixing #4647).
agda · May 18, 2020 · 4522e7a · 4522e7a
1 parent 5e7016c
commit 4522e7a
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 10 deletions.
diff --git a/test/interaction/Issue1804.out b/test/interaction/Issue1804.out
@@ -8,4 +8,4 @@
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
 (agda2-status-action "Checked")
-(agda2-info-action "*Scope Info*" "F is not in scope." nil)
+(agda2-info-action "*Scope Info*" "F is in scope as * a record field Issue1804._.F brought into scope by - the application of R at Issue1804.agda:8,6-7 - its definition at Issue1804.agda:4,9-10" nil)
diff --git a/test/interaction/TopScope.out b/test/interaction/TopScope.out
@@ -13,21 +13,18 @@
 (agda2-status-action "")
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
-(agda2-info-action "*Error*" "1,1-7 Not in scope: unused at 1,1-7 when scope checking unused" nil)
-(agda2-highlight-load-and-delete-action)
-(agda2-status-action "")
+(agda2-status-action "Checked")
+(agda2-info-action "*Inferred Type*" "Bool" nil)
 (agda2-status-action "")
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
-(agda2-info-action "*Error*" "1,1-5 Not in scope: used at 1,1-5 when scope checking used" nil)
-(agda2-highlight-load-and-delete-action)
-(agda2-status-action "")
+(agda2-status-action "Checked")
+(agda2-info-action "*Inferred Type*" "Bool" nil)
 (agda2-status-action "")
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
-(agda2-info-action "*Error*" "1,1-21 Not in scope: Private.not-in-scope at 1,1-21 (did you mean 'in-scope'?) when scope checking Private.not-in-scope" nil)
-(agda2-highlight-load-and-delete-action)
-(agda2-status-action "")
+(agda2-status-action "Checked")
+(agda2-info-action "*Inferred Type*" "Bool" nil)
 (agda2-status-action "")
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)