Move screen details into StackSet

This commit is contained in:
Spencer Janssen 2007-06-29 21:39:17 +00:00
parent bb12b08239
commit ab830ec227
5 changed files with 99 additions and 90 deletions

View File

@ -52,7 +52,8 @@ main = do
let winset | ("--resume" : s : _) <- args
, [(x, "")] <- reads s = x
| otherwise = new [0..fromIntegral workspaces-1] (fromIntegral $ length xinesc)
| otherwise = new [0..fromIntegral workspaces-1] $ zipWith SD xinesc gaps
gaps = take (length xinesc) $ defaultGaps ++ repeat (0,0,0,0)
safeLayouts = case defaultLayouts of [] -> (full, []); (x:xs) -> (x,xs)
cf = XConf
@ -63,8 +64,6 @@ main = do
st = XState
{ windowset = winset
, layouts = M.fromList [(w, safeLayouts) | w <- [0 .. W workspaces - 1]]
, statusGaps = take (length xinesc) $ defaultGaps ++ repeat (0,0,0,0)
, xineScreens = xinesc
, mapped = S.empty
, waitingUnmap = M.empty }

View File

@ -21,7 +21,7 @@ import qualified StackSet as W
import {-# SOURCE #-} Config (borderWidth,logHook,numlockMask)
import Data.Maybe
import Data.List (genericIndex, nub, (\\), findIndex)
import Data.List (nub, (\\), find)
import Data.Bits ((.|.), (.&.), complement)
import Data.Ratio
import qualified Data.Map as M
@ -98,11 +98,10 @@ view = windows . W.view
-- Taking a function giving the current screen, and current geometry.
modifyGap :: (Int -> (Int,Int,Int,Int) -> (Int,Int,Int,Int)) -> X ()
modifyGap f = do
XState { windowset = ws, statusGaps = gaps } <- get
let n = fromIntegral . W.screen $ W.current ws
(a,i:b) = splitAt n gaps
modify $ \s -> s { statusGaps = a ++ f n i : b }
refresh
windows $ \ws@(W.StackSet { W.current = c@(W.Screen { W.screenDetail = sd }) }) ->
let n = fromIntegral . W.screen $ c
g = f n . statusGap $ sd
in ws { W.current = c { W.screenDetail = sd { statusGap = g } } }
-- | Kill the currently focused client. If we do kill it, we'll get a
-- delete notify back from X.
@ -135,7 +134,7 @@ windows f = do
-- We cannot use sendMessage because this must not call refresh ever,
-- and must be called on all visible workspaces.
broadcastMessage UnDoLayout
XState { windowset = old, layouts = fls, xineScreens = xinesc, statusGaps = gaps } <- get
XState { windowset = old, layouts = fls } <- get
let oldvisible = concatMap (W.integrate' . W.stack . W.workspace) $ W.current old : W.visible old
ws = f old
modify (\s -> s { windowset = ws })
@ -149,8 +148,8 @@ windows f = do
flt = filter (flip M.member (W.floating ws)) (W.index this)
tiled = (W.stack . W.workspace . W.current $ this)
>>= W.filter (not . flip M.member (W.floating ws))
(Rectangle sx sy sw sh) = genericIndex xinesc (W.screen w)
(gt,gb,gl,gr) = genericIndex gaps (W.screen w)
(SD (Rectangle sx sy sw sh)
(gt,gb,gl,gr)) = W.screenDetail w
viewrect = Rectangle (sx + fromIntegral gl) (sy + fromIntegral gt)
(sw - fromIntegral (gl + gr)) (sh - fromIntegral (gt + gb))
@ -257,13 +256,13 @@ rescreen :: X ()
rescreen = do
xinesc <- withDisplay (io . getScreenInfo)
modify (\s -> s { xineScreens = xinesc
, statusGaps = take (length xinesc) $ (statusGaps s) ++ repeat (0,0,0,0) })
windows $ \ws@(W.StackSet { W.current = v, W.visible = vs, W.hidden = hs }) ->
let (x:xs, ys) = splitAt (length xinesc) $ map W.workspace (v:vs) ++ hs
in ws { W.current = W.Screen x 0
, W.visible = zipWith W.Screen xs [1 ..]
let (xs, ys) = splitAt (length xinesc) $ map W.workspace (v:vs) ++ hs
(a:as) = zipWith3 W.Screen xs [1..] $ zipWith SD xinesc gs
sgs = map (statusGap . W.screenDetail) (v:vs)
gs = take (length xinesc) (sgs ++ repeat (0,0,0,0))
in ws { W.current = a
, W.visible = as
, W.hidden = ys }
-- ---------------------------------------------------------------------
@ -476,20 +475,19 @@ sink = windows . W.sink
-- | Make a tiled window floating, using its suggested rectangle
float :: Window -> X ()
float w = withDisplay $ \d -> do
XState { xineScreens = xinesc, windowset = ws } <- get
ws <- gets windowset
wa <- io $ getWindowAttributes d w
let sid = fromMaybe (W.screen . W.current $ ws) (fmap fi $ findIndex (pointWithin (fi (wa_x wa)) (fi (wa_y wa))) xinesc)
sc = genericIndex xinesc sid
let sc = fromMaybe (W.current ws) $ find (pointWithin (fi $ wa_x wa) (fi $ wa_y wa) . screenRect . W.screenDetail) $ W.current ws : W.visible ws
sr = screenRect . W.screenDetail $ sc
sw = W.tag . W.workspace $ sc
bw = fi . wa_border_width $ wa
wid <- screenWorkspace sid
windows $ W.shift wid . W.focusWindow w . W.float w
(W.RationalRect ((fi (wa_x wa) - fi (rect_x sc)) % fi (rect_width sc))
((fi (wa_y wa) - fi (rect_y sc)) % fi (rect_height sc))
(fi (wa_width wa + bw*2) % fi (rect_width sc))
(fi (wa_height wa + bw*2) % fi (rect_height sc)))
windows $ W.shift sw . W.focusWindow w . W.float w
(W.RationalRect ((fi (wa_x wa) - fi (rect_x sr)) % fi (rect_width sr))
((fi (wa_y wa) - fi (rect_y sr)) % fi (rect_height sr))
(fi (wa_width wa + bw*2) % fi (rect_width sr))
(fi (wa_height wa + bw*2) % fi (rect_height sr)))
where fi x = fromIntegral x
pointWithin :: Integer -> Integer -> Rectangle -> Bool
pointWithin x y r = x >= fi (rect_x r) &&

View File

@ -37,7 +37,7 @@ module StackSet (
import Prelude hiding (filter)
import Data.Maybe (listToMaybe)
import qualified Data.List as L (delete,find,genericSplitAt,filter)
import qualified Data.List as L (delete,deleteBy,find,splitAt,filter)
import qualified Data.Map as M (Map,insert,delete,empty)
-- $intro
@ -146,15 +146,17 @@ import qualified Data.Map as M (Map,insert,delete,empty)
-- that are produced are used to track those workspaces visible as
-- Xinerama screens, and those workspaces not visible anywhere.
data StackSet i a sid =
StackSet { current :: !(Screen i a sid) -- ^ currently focused workspace
, visible :: [Screen i a sid] -- ^ non-focused workspaces, visible in xinerama
data StackSet i a sid sd =
StackSet { current :: !(Screen i a sid sd) -- ^ currently focused workspace
, visible :: [Screen i a sid sd] -- ^ non-focused workspaces, visible in xinerama
, hidden :: [Workspace i a] -- ^ workspaces not visible anywhere
, floating :: M.Map a RationalRect -- ^ floating windows
} deriving (Show, Read, Eq)
-- | Visible workspaces, and their Xinerama screens.
data Screen i a sid = Screen { workspace :: !(Workspace i a), screen :: !sid }
data Screen i a sid sd = Screen { workspace :: !(Workspace i a)
, screen :: !sid
, screenDetail :: !sd }
deriving (Show, Read, Eq)
-- |
@ -205,10 +207,10 @@ abort x = error $ "xmonad: StackSet: " ++ x
--
-- Xinerama: Virtual workspaces are assigned to physical screens, starting at 0.
--
new :: Integral s => [i] -> s -> StackSet i a s
new (wid:wids) m | m > 0 = StackSet cur visi unseen M.empty
where (seen,unseen) = L.genericSplitAt m $ Workspace wid Nothing : [ Workspace i Nothing | i <- wids]
(cur:visi) = [ Screen i s | (i,s) <- zip seen [0..] ]
new :: (Integral s) => [i] -> [sd] -> StackSet i a s sd
new wids m | not (null wids) && length m <= length wids = StackSet cur visi unseen M.empty
where (seen,unseen) = L.splitAt (length m) $ map (flip Workspace Nothing) wids
(cur:visi) = [ Screen i s sd | (i, s, sd) <- zip3 seen [0..] m ]
-- now zip up visibles with their screen id
new _ _ = abort "non-positive argument to StackSet.new"
@ -222,21 +224,22 @@ new _ _ = abort "non-positive argument to StackSet.new"
-- becomes the current screen. If it is in the visible list, it becomes
-- current.
view :: (Eq a, Eq s, Eq i) => i -> StackSet i a s -> StackSet i a s
view :: (Eq a, Eq s, Eq i) => i -> StackSet i a s sd -> StackSet i a s sd
view i s
| not (elem i $ map tag $ workspaces s)
|| i == tag (workspace (current s)) = s -- out of bounds or current
| Just x <- L.find ((i==).tag.workspace) (visible s)
-- if it is visible, it is just raised
= s { current = x, visible = current s : L.delete x (visible s) }
= s { current = x, visible = current s : L.deleteBy screenEq x (visible s) }
| Just x <- L.find ((i==).tag) (hidden s)
-- if it was hidden, it is raised on the xine screen currently used
= s { current = Screen x (screen (current s))
= s { current = (current s) { workspace = x }
, hidden = workspace (current s) : L.delete x (hidden s) }
| otherwise = s
where screenEq x y = screen x == screen y
-- 'Catch'ing this might be hard. Relies on monotonically increasing
-- workspace tags defined in 'new'
@ -246,8 +249,8 @@ view i s
-- | Find the tag of the workspace visible on Xinerama screen 'sc'.
-- Nothing if screen is out of bounds.
lookupWorkspace :: Eq s => s -> StackSet i a s -> Maybe i
lookupWorkspace sc w = listToMaybe [ tag i | Screen i s <- current w : visible w, s == sc ]
lookupWorkspace :: Eq s => s -> StackSet i a s sd -> Maybe i
lookupWorkspace sc w = listToMaybe [ tag i | Screen i s _ <- current w : visible w, s == sc ]
-- ---------------------------------------------------------------------
-- $stackOperations
@ -258,13 +261,13 @@ lookupWorkspace sc w = listToMaybe [ tag i | Screen i s <- current w : visible w
-- default value. Otherwise, it applies the function to the stack,
-- returning the result. It is like 'maybe' for the focused workspace.
--
with :: b -> (Stack a -> b) -> StackSet i a s -> b
with :: b -> (Stack a -> b) -> StackSet i a s sd -> b
with dflt f = maybe dflt f . stack . workspace . current
-- |
-- Apply a function, and a default value for Nothing, to modify the current stack.
--
modify :: StackOrNot a -> (Stack a -> StackOrNot a) -> StackSet i a s -> StackSet i a s
modify :: StackOrNot a -> (Stack a -> StackOrNot a) -> StackSet i a s sd -> StackSet i a s sd
modify d f s = s { current = (current s)
{ workspace = (workspace (current s)) { stack = with d f s }}}
@ -272,14 +275,14 @@ modify d f s = s { current = (current s)
-- Apply a function to modify the current stack if it isn't empty, and we don't
-- want to empty it.
--
modify' :: (Stack a -> Stack a) -> StackSet i a s -> StackSet i a s
modify' :: (Stack a -> Stack a) -> StackSet i a s sd -> StackSet i a s sd
modify' f = modify Nothing (Just . f)
-- |
-- /O(1)/. Extract the focused element of the current stack.
-- Return Just that element, or Nothing for an empty stack.
--
peek :: StackSet i a s -> Maybe a
peek :: StackSet i a s sd -> Maybe a
peek = with Nothing (return . focus)
-- |
@ -321,7 +324,7 @@ filter p (Stack f ls rs) = case L.filter p (f:rs) of
-- the head of the list. The implementation is given by the natural
-- integration of a one-hole list cursor, back to a list.
--
index :: Eq a => StackSet i a s -> [a]
index :: Eq a => StackSet i a s sd -> [a]
index = with [] integrate
-- let is = t : r ++ reverse l in take (length is) (dropWhile (/= m) (cycle is))
@ -338,7 +341,7 @@ index = with [] integrate
-- if we reach the end. Again the wrapping model should 'cycle' on
-- the current stack.
--
focusUp, focusDown, swapUp, swapDown :: StackSet i a s -> StackSet i a s
focusUp, focusDown, swapUp, swapDown :: StackSet i a s sd -> StackSet i a s sd
focusUp = modify' focusUp'
focusDown = modify' (reverseStack . focusUp' . reverseStack)
@ -360,7 +363,7 @@ reverseStack (Stack t ls rs) = Stack t rs ls
-- | /O(1) on current window, O(n) in general/. Focus the window 'w',
-- and set its workspace as current.
--
focusWindow :: (Integral i, Eq s, Eq a) => a -> StackSet i a s -> StackSet i a s
focusWindow :: (Integral i, Eq s, Eq a) => a -> StackSet i a s sd -> StackSet i a s sd
focusWindow w s | Just w == peek s = s
| otherwise = maybe s id $ do
n <- findIndex w s
@ -369,11 +372,11 @@ focusWindow w s | Just w == peek s = s
-- | Get a list of all workspaces in the StackSet.
workspaces :: StackSet i a s -> [Workspace i a]
workspaces :: StackSet i a s sd -> [Workspace i a]
workspaces s = workspace (current s) : map workspace (visible s) ++ hidden s
-- | Is the given tag present in the StackSet?
tagMember :: Eq i => i -> StackSet i a s -> Bool
tagMember :: Eq i => i -> StackSet i a s sd -> Bool
tagMember t = elem t . map tag . workspaces
-- |
@ -382,13 +385,13 @@ tagMember t = elem t . map tag . workspaces
--
-- | /O(n)/. Is a window in the StackSet.
member :: Eq a => a -> StackSet i a s -> Bool
member :: Eq a => a -> StackSet i a s sd -> Bool
member a s = maybe False (const True) (findIndex a s)
-- | /O(1) on current window, O(n) in general/.
-- Return Just the workspace index of the given window, or Nothing
-- if the window is not in the StackSet.
findIndex :: Eq a => a -> StackSet i a s -> Maybe i
findIndex :: Eq a => a -> StackSet i a s sd -> Maybe i
findIndex a s = listToMaybe
[ tag w | w <- workspaces s, has a (stack w) ]
where has _ Nothing = False
@ -411,11 +414,11 @@ findIndex a s = listToMaybe
-- Semantics in Huet's paper is that insert doesn't move the cursor.
-- However, we choose to insert above, and move the focus.
--
insertUp :: Eq a => a -> StackSet i a s -> StackSet i a s
insertUp :: Eq a => a -> StackSet i a s sd -> StackSet i a s sd
insertUp a s = if member a s then s else insert
where insert = modify (Just $ Stack a [] []) (\(Stack t l r) -> Just $ Stack a l (t:r)) s
-- insertDown :: a -> StackSet i a s -> StackSet i a s
-- insertDown :: a -> StackSet i a s sd -> StackSet i a s sd
-- insertDown a = modify (Stack a [] []) $ \(Stack t l r) -> Stack a (t:l) r
-- Old semantics, from Huet.
-- > w { down = a : down w }
@ -434,7 +437,7 @@ insertUp a s = if member a s then s else insert
-- * deleting the master window resets it to the newly focused window
-- * otherwise, delete doesn't affect the master.
--
delete :: (Integral i, Ord a, Eq s) => a -> StackSet i a s -> StackSet i a s
delete :: (Integral i, Ord a, Eq s) => a -> StackSet i a s sd -> StackSet i a s sd
delete w s | Just w == peek s = remove s -- common case.
| otherwise = maybe s (removeWindow.tag.workspace.current $ s) (findIndex w s)
where
@ -454,11 +457,11 @@ delete w s | Just w == peek s = remove s -- common case.
-- | Given a window, and its preferred rectangle, set it as floating
-- A floating window should already be managed by the StackSet.
float :: Ord a => a -> RationalRect -> StackSet i a s -> StackSet i a s
float :: Ord a => a -> RationalRect -> StackSet i a s sd -> StackSet i a s sd
float w r s = s { floating = M.insert w r (floating s) }
-- | Clear the floating status of a window
sink :: Ord a => a -> StackSet i a s -> StackSet i a s
sink :: Ord a => a -> StackSet i a s sd -> StackSet i a s sd
sink w s = s { floating = M.delete w (floating s) }
------------------------------------------------------------------------
@ -467,7 +470,7 @@ sink w s = s { floating = M.delete w (floating s) }
-- | /O(s)/. Set the master window to the focused window.
-- The old master window is swapped in the tiling order with the focused window.
-- Focus stays with the item moved.
swapMaster :: StackSet i a s -> StackSet i a s
swapMaster :: StackSet i a s sd -> StackSet i a s sd
swapMaster = modify' $ \c -> case c of
Stack _ [] _ -> c -- already master.
Stack t ls rs -> Stack t [] (ys ++ x : rs) where (x:ys) = reverse ls
@ -483,7 +486,7 @@ swapMaster = modify' $ \c -> case c of
-- The actual focused workspace doesn't change. If there is -- no
-- element on the current stack, the original stackSet is returned.
--
shift :: (Ord a, Eq s, Integral i) => i -> StackSet i a s -> StackSet i a s
shift :: (Ord a, Eq s, Integral i) => i -> StackSet i a s sd -> StackSet i a s sd
shift n s = if and [n >= 0,n `tagMember` s, n /= tag (workspace (current s))]
then maybe s go (peek s) else s
where go w = foldr ($) s [view (tag (workspace (current s))),insertUp w,view n,delete w]

View File

@ -15,7 +15,7 @@
-----------------------------------------------------------------------------
module XMonad (
X, WindowSet, WorkspaceId(..), ScreenId(..), XState(..), XConf(..), Layout(..),
X, WindowSet, WorkspaceId(..), ScreenId(..), ScreenDetail(..), XState(..), XConf(..), Layout(..),
Typeable, Message, SomeMessage(..), fromMessage, runLayout,
runX, catchX, io, catchIO, withDisplay, withWindowSet, isRoot, spawn, restart, trace, whenJust, whenX,
atom_WM_STATE, atom_WM_PROTOCOLS, atom_WM_DELETE_WINDOW
@ -30,6 +30,8 @@ import System.Posix.Process (executeFile, forkProcess, getProcessStatus, createS
import System.Exit
import System.Environment
import Graphics.X11.Xlib
-- for Read instance
import Graphics.X11.Xlib.Extras ()
import Data.Typeable
import qualified Data.Map as M
@ -39,8 +41,6 @@ import qualified Data.Set as S
-- Just the display, width, height and a window list
data XState = XState
{ windowset :: !WindowSet -- ^ workspace list
, xineScreens :: ![Rectangle] -- ^ dimensions of each screen
, statusGaps :: ![(Int,Int,Int,Int)] -- ^ width of status bar on each screen
, mapped :: !(S.Set Window) -- ^ the Set of mapped windows
, waitingUnmap :: !(M.Map Window Int) -- ^ the number of expected UnmapEvents
, layouts :: !(M.Map WorkspaceId (Layout Window, [Layout Window])) }
@ -51,7 +51,7 @@ data XConf = XConf
, normalBorder :: !Pixel -- ^ border color of unfocused windows
, focusedBorder :: !Pixel } -- ^ border color of the focused window
type WindowSet = StackSet WorkspaceId Window ScreenId
type WindowSet = StackSet WorkspaceId Window ScreenId ScreenDetail
-- | Virtual workspace indicies
newtype WorkspaceId = W Int deriving (Eq,Ord,Show,Read,Enum,Num,Integral,Real)
@ -59,6 +59,10 @@ newtype WorkspaceId = W Int deriving (Eq,Ord,Show,Read,Enum,Num,Integral,Real)
-- | Physical screen indicies
newtype ScreenId = S Int deriving (Eq,Ord,Show,Read,Enum,Num,Integral,Real)
data ScreenDetail = SD { screenRect :: !Rectangle
, statusGap :: !(Int,Int,Int,Int) -- ^ width of status bar on the screen
} deriving (Eq,Show, Read)
------------------------------------------------------------------------
-- | The X monad, a StateT transformer over IO encapsulating the window

View File

@ -33,11 +33,13 @@ import qualified Data.Map as M
--
-- The all important Arbitrary instance for StackSet.
--
instance (Integral i, Integral s, Eq a, Arbitrary a) => Arbitrary (StackSet i a s) where
instance (Integral i, Integral s, Eq a, Arbitrary a, Arbitrary sd)
=> Arbitrary (StackSet i a s sd) where
arbitrary = do
sz <- choose (1,10) -- number of workspaces
n <- choose (0,sz-1) -- pick one to be in focus
sc <- choose (1,sz) -- a number of physical screens
sc <- choose (1,sz) -- a number of physical screens
sds <- replicateM sc arbitrary
ls <- vector sz -- a vector of sz workspaces
-- pick a random item in each stack to focus
@ -45,7 +47,7 @@ instance (Integral i, Integral s, Eq a, Arbitrary a) => Arbitrary (StackSet i a
else liftM Just (choose ((-1),length s-1))
| s <- ls ]
return $ fromList (fromIntegral n, fromIntegral sc,fs,ls)
return $ fromList (fromIntegral n, sds,fs,ls)
coarbitrary = error "no coarbitrary for StackSet"
@ -59,14 +61,9 @@ instance (Integral i, Integral s, Eq a, Arbitrary a) => Arbitrary (StackSet i a
-- 'fs' random focused window on each workspace
-- 'xs' list of list of windows
--
fromList :: (Integral i, Integral s, Eq a) => (i, s, [Maybe Int], [[a]]) -> StackSet i a s
fromList :: (Integral i, Integral s, Eq a) => (i, [sd], [Maybe Int], [[a]]) -> StackSet i a s sd
fromList (_,_,_,[]) = error "Cannot build a StackSet from an empty list"
fromList (n,m,fs,xs) | n < 0 || n >= genericLength xs
= error $ "Cursor index is out of range: " ++ show (n, length xs)
| m < 1 || m > genericLength xs
= error $ "Can't have more screens than workspaces: " ++ show (m, length xs)
fromList (o,m,fs,xs) =
let s = view o $
foldr (\(i,ys) s ->
@ -81,7 +78,7 @@ fromList (o,m,fs,xs) =
--
-- Just generate StackSets with Char elements.
--
type T = StackSet (NonNegative Int) Char Int
type T = StackSet (NonNegative Int) Char Int Int
-- Useful operation, the non-local workspaces
hidden_spaces x = map workspace (visible x) ++ hidden x
@ -131,8 +128,9 @@ monotonic (x:y:zs) | x == y-1 = monotonic (y:zs)
prop_invariant = invariant
-- and check other ops preserve invariants
prop_empty_I (n :: Positive Int) = forAll (choose (1,fromIntegral n)) $ \m ->
invariant $ new [0..fromIntegral n-1] m
prop_empty_I (n :: Positive Int) = forAll (choose (1,fromIntegral n)) $ \m ->
forAll (vector m) $ \ms ->
invariant $ new [0..fromIntegral n-1] ms
prop_view_I (n :: NonNegative Int) (x :: T) =
n `tagMember` x ==> invariant $ view (fromIntegral n) x
@ -170,19 +168,20 @@ prop_shift_I (n :: NonNegative Int) (x :: T) =
-- 'new'
-- empty StackSets have no windows in them
prop_empty (NonEmptyNubList ns) (m :: Positive Int) =
all (== Nothing) [ stack w | w <- workspace (current x)
prop_empty (EmptyStackSet x) =
all (== Nothing) [ stack w | w <- workspace (current x)
: map workspace (visible x) ++ hidden x ]
where x = new ns (fromIntegral m) :: T
-- empty StackSets always have focus on first workspace
prop_empty_current (NonEmptyNubList ns) (m :: Positive Int) = tag (workspace $ current x) == head ns
where x = new ns (fromIntegral m) :: T
prop_empty_current (NonEmptyNubList ns) (NonEmptyNubList sds) =
-- TODO, this is ugly
length sds <= length ns ==>
tag (workspace $ current x) == head ns
where x = new ns sds :: T
-- no windows will be a member of an empty workspace
prop_member_empty i (NonEmptyNubList ns) (m :: Positive Int)
= member i (new ns (fromIntegral m) :: T) == False
prop_member_empty i (EmptyStackSet x)
= member i x == False
-- ---------------------------------------------------------------------
-- viewing workspaces
@ -320,8 +319,7 @@ prop_findIndex (x :: T) =
-- 'insert'
-- inserting a item into an empty stackset means that item is now a member
prop_insert_empty i (NonEmptyNubList ns) (m :: Positive Int) = member i (insertUp i x)
where x = new ns (fromIntegral m) :: T
prop_insert_empty i (EmptyStackSet x)= member i (insertUp i x)
-- insert should be idempotent
prop_insert_idem i (x :: T) = insertUp i x == insertUp i (insertUp i x)
@ -334,9 +332,8 @@ prop_insert_local (x :: T) i = not (member i x) ==> hidden_spaces x == hidden_sp
-- Inserting a (unique) list of items into an empty stackset should
-- result in the last inserted element having focus.
prop_insert_peek (NonEmptyNubList ns) (m :: Positive Int) (NonEmptyNubList is) =
prop_insert_peek (EmptyStackSet x) (NonEmptyNubList is) =
peek (foldr insertUp x is) == Just (head is)
where x = new ns (fromIntegral m) :: T
-- insert >> delete is the identity, when i `notElem` .
-- Except for the 'master', which is reset on insert and delete.
@ -347,11 +344,10 @@ prop_insert_delete n x = not (member n x) ==> delete n (insertUp n y) == (y :: T
-- otherwise, we don't have a rule for where master goes.
-- inserting n elements increases current stack size by n
prop_size_insert is (NonEmptyNubList ns) (m :: Positive Int) =
prop_size_insert is (EmptyStackSet x) =
size (foldr insertUp x ws ) == (length ws)
where
ws = nub is
x = new ns (fromIntegral m) :: T
size = length . index
@ -731,6 +727,15 @@ instance (Num a, Ord a, Arbitrary a) => Arbitrary (NonNegative a) where
]
coarbitrary = undefined
newtype EmptyStackSet = EmptyStackSet T deriving Show
instance Arbitrary EmptyStackSet where
arbitrary = do
(NonEmptyNubList ns) <- arbitrary
(NonEmptyNubList sds) <- arbitrary
-- there cannot be more screens than workspaces:
return . EmptyStackSet . new ns $ take (min (length ns) (length sds)) sds
-- | Generates a value that satisfies a predicate.
suchThat :: Gen a -> (a -> Bool) -> Gen a
gen `suchThat` p =