droundy:

Hi all,

Here's a cut at a focus stack. It's a bit crude, but seems to work. I had to tweak the rotate properties, since rotating the focus (obviously) changes the focus stack. I don't think this weakening of those checks is really a Bad Thing. And I'm a little puzzled how prop_delete_push ever passed. Maybe it failed, and noone noticed? Or maybe we aren't running enough tests with large enough stack sizes, so we never ran into the case where the focus wasn't on the master window to start with? I don't know, but it suggests something is wrong.

Yes. Thanks for thinking about this! Fixing the Arbitrary StackSet instance to set focus randomly on each workspace, fs <- sequence [ if null s then return Nothing else liftM Just (elements s) | s <- ls ] And then folding focus over each stac: foldr (\f s -> case f of Nothing -> s Just w -> raiseFocus w s) s fs We now have 3 QC properties failing, including the one making claims about the behaviour of focus/delete/push: 1 delete.push identity : Falsifiable after 2 tests 2 shift reversible : Falsifiable after 1 tests 3 promote only swaps : Falsifiable after 8 tests For 1. we know this is a bug wrt. what we want to implement, in terms of where focus goes on push >> delete. The others are likely to just be overly constrained QC properties. -- Don