diff options
| -rw-r--r-- | Main.hs | 5 | ||||
| -rw-r--r-- | Operations.hs | 48 | ||||
| -rw-r--r-- | StackSet.hs | 67 | ||||
| -rw-r--r-- | XMonad.hs | 12 | ||||
| -rw-r--r-- | tests/Properties.hs | 57 |
5 files changed, 99 insertions, 90 deletions
@@ -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 } diff --git a/Operations.hs b/Operations.hs index 2bb348a..ee5a5bc 100644 --- a/Operations.hs +++ b/Operations.hs @@ -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) && diff --git a/StackSet.hs b/StackSet.hs index 3d369f9..037b124 100644 --- a/StackSet.hs +++ b/StackSet.hs @@ -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] @@ -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 diff --git a/tests/Properties.hs b/tests/Properties.hs index c96dcc0..452267f 100644 --- a/tests/Properties.hs +++ b/tests/Properties.hs @@ -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 = |