Skip to content

Commit

Permalink
[ #4647 ] broken tests
Browse files Browse the repository at this point in the history
These interaction tests are broken by the fix of #4647, due to the
additional reloads triggered by top-level commands.

Solutions given to metas by interaction commands get lost by reloads,
since they are not incorporated into the source file (naturally).  The
situation is now similar to why case splits do no update the state of
the interaction.
  • Loading branch information
andreasabel committed May 13, 2020
1 parent c26b994 commit bb01ef9
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 2 deletions.
5 changes: 4 additions & 1 deletion test/interaction/ExtendedLambdaCase.out
Expand Up @@ -5,7 +5,10 @@
(agda2-info-action "*All Goals*" "?0 : Bool ?1 : Bool ?2 : Bool ?3 : Bool ?4 : A → {x : A} → A → A " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4)))
(agda2-status-action "")
(agda2-info-action "*Normal Form*" "(y : Bool) → parameterised.Bar (λ _ → Void) (λ { true → true ; false → false })" nil)
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*Normal Form*" "(x : Bool) → parameterised.Bar (λ _ → Void) (λ { true → true ; false → false })" nil)
(agda2-give-action 4 "λ { a {x} b → a }")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Bool ?1 : Bool ?2 : Bool ?3 : Bool " nil)
Expand Down
2 changes: 1 addition & 1 deletion test/interaction/Long.out
Expand Up @@ -92,10 +92,10 @@
(agda2-status-action "")
(agda2-info-action "*Inferred Type*" "Maybe Nat" nil)
(agda2-status-action "")
(agda2-info-action "*Normal Form*" "Nothing" nil)
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*Normal Form*" "?1" nil)
(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
Expand Down

0 comments on commit bb01ef9

Please sign in to comment.