Skip to content

Commit

Permalink
StateModel: don't .before on undefined (fixes coq#273)
Browse files Browse the repository at this point in the history
In an attempt to improve errors in the goal window, coq#184 was recently
mereged. Unfortunately, it is broken. The fix is guaring the unfocused
goals check with a simple assertion on state.backgroundGoals.

Signed-off-by: Ramkumar Ramachandra <r@artagnon.com>
  • Loading branch information
artagnon authored and Blaisorblade committed Mar 9, 2022
1 parent bdbca83 commit 163cdd8
Showing 1 changed file with 6 additions and 4 deletions.
10 changes: 6 additions & 4 deletions html_views/src/goals/StateModel.ts
Original file line number Diff line number Diff line change
Expand Up @@ -189,17 +189,19 @@ export class StateModel {
, createFocusedGoals(state.goals)
])
var elmnt = document.getElementById("firstGoal");
elmnt.scrollIntoView({block: "center", inline: "nearest"});
} else if (state.backgroundGoals.before.length > 0 || state.backgroundGoals.after.length > 0 || state.backgroundGoals.next != undefined ) {
this.setMessage("There are unfocused goals.");
elmnt.scrollIntoView({block: "center", inline: "nearest"});
} else if (state.backgroundGoals) {
if (state.backgroundGoals.before.length > 0 || state.backgroundGoals.after.length > 0 || state.backgroundGoals.next) {
this.setMessage("There are unfocused goals.");
}
} else if (state.shelvedGoals.length > 0 ) {
this.setMessage("There are shelved goals. Try using `Unshelve`.");
} else if (state.abandonedGoals.length > 0 ) {
this.setMessage("There are some goals you gave up. You need to go back and solve them, or use `Admitted.`.")
} else
this.setMessage("No more subgoals. Internal invariant violated. Please report.")
}

if(hasSubstitutions)
$('#togglePrettifySymbols').removeClass("hidden")
else
Expand Down

0 comments on commit 163cdd8

Please sign in to comment.