summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorSpencer Janssen <sjanssen@cse.unl.edu>2007-06-29 23:39:17 +0200
committerSpencer Janssen <sjanssen@cse.unl.edu>2007-06-29 23:39:17 +0200
commitccc8377b43ca258b30d37402bdcf881e9acab7d9 (patch)
treed938fa4d290b5d324229fdf915b36ae6b86d6d45
parent2ea97e792f3584981ea565ec960d75a0568665f5 (diff)
downloadmetatile-ccc8377b43ca258b30d37402bdcf881e9acab7d9.tar
metatile-ccc8377b43ca258b30d37402bdcf881e9acab7d9.zip
Move screen details into StackSet
darcs-hash:20070629213917-a5988-3ad31d8f028efcec41c9c4805c01c2d42c0009b2
-rw-r--r--Main.hs5
-rw-r--r--Operations.hs48
-rw-r--r--StackSet.hs67
-rw-r--r--XMonad.hs12
-rw-r--r--tests/Properties.hs57
5 files changed, 99 insertions, 90 deletions
diff --git a/Main.hs b/Main.hs
index 156cea7..64929c5 100644
--- a/Main.hs
+++ b/Main.hs
@@ -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]
diff --git a/XMonad.hs b/XMonad.hs
index bc54bfd..8eec7b1 100644
--- a/XMonad.hs
+++ b/XMonad.hs
@@ -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 =