mirror of
https://github.com/xmonad/xmonad.git
synced 2025-05-19 08:30:21 -07:00
make focus, up and down complete functions.
This is a rerun of my change to make (Stack a) never be empty. Gives us more type-safety.
This commit is contained in:
parent
4ffee115e1
commit
5f8202e79e
4
Main.hs
4
Main.hs
@ -88,11 +88,11 @@ main = do
|
|||||||
-- TODO, general iterators for these lists.
|
-- TODO, general iterators for these lists.
|
||||||
sequence_ [ setInitialProperties w >> reveal w
|
sequence_ [ setInitialProperties w >> reveal w
|
||||||
| wk <- map W.workspace (W.current winset : W.visible winset)
|
| wk <- map W.workspace (W.current winset : W.visible winset)
|
||||||
, w <- W.integrate (W.stack wk) ]
|
, w <- W.integrate' (W.stack wk) ]
|
||||||
|
|
||||||
sequence_ [ setInitialProperties w >> hide w
|
sequence_ [ setInitialProperties w >> hide w
|
||||||
| wk <- W.hidden winset
|
| wk <- W.hidden winset
|
||||||
, w <- W.integrate (W.stack wk) ]
|
, w <- W.integrate' (W.stack wk) ]
|
||||||
|
|
||||||
mapM_ manage ws -- find new windows
|
mapM_ manage ws -- find new windows
|
||||||
logHook
|
logHook
|
||||||
|
@ -134,7 +134,7 @@ windows f = do
|
|||||||
-- and must be called on all visible workspaces.
|
-- and must be called on all visible workspaces.
|
||||||
broadcastMessage UnDoLayout
|
broadcastMessage UnDoLayout
|
||||||
XState { windowset = old, layouts = fls, xineScreens = xinesc, statusGaps = gaps } <- get
|
XState { windowset = old, layouts = fls, xineScreens = xinesc, statusGaps = gaps } <- get
|
||||||
let oldvisible = concatMap (W.integrate . W.stack . W.workspace) $ W.current old : W.visible old
|
let oldvisible = concatMap (W.integrate' . W.stack . W.workspace) $ W.current old : W.visible old
|
||||||
ws = f old
|
ws = f old
|
||||||
modify (\s -> s { windowset = ws })
|
modify (\s -> s { windowset = ws })
|
||||||
d <- asks display
|
d <- asks display
|
||||||
@ -145,8 +145,7 @@ windows f = do
|
|||||||
this = W.view n ws
|
this = W.view n ws
|
||||||
Just l = fmap fst $ M.lookup n fls
|
Just l = fmap fst $ M.lookup n fls
|
||||||
flt = filter (flip M.member (W.floating ws)) (W.index this)
|
flt = filter (flip M.member (W.floating ws)) (W.index this)
|
||||||
tiled = W.filter (not . flip M.member (W.floating ws))
|
tiled = W.filter (not . flip M.member (W.floating ws)) . W.stack . W.workspace . W.current $ this
|
||||||
. W.stack . W.workspace . W.current $ this
|
|
||||||
(Rectangle sx sy sw sh) = genericIndex xinesc (W.screen w)
|
(Rectangle sx sy sw sh) = genericIndex xinesc (W.screen w)
|
||||||
(gt,gb,gl,gr) = genericIndex gaps (W.screen w)
|
(gt,gb,gl,gr) = genericIndex gaps (W.screen w)
|
||||||
viewrect = Rectangle (sx + fromIntegral gl) (sy + fromIntegral gt)
|
viewrect = Rectangle (sx + fromIntegral gl) (sy + fromIntegral gt)
|
||||||
@ -154,7 +153,7 @@ windows f = do
|
|||||||
|
|
||||||
-- just the tiled windows:
|
-- just the tiled windows:
|
||||||
-- now tile the windows on this workspace, modified by the gap
|
-- now tile the windows on this workspace, modified by the gap
|
||||||
rs <- doLayout l viewrect tiled -- `mplus` doLayout full viewrect tiled
|
rs <- runLayout l viewrect tiled -- `mplus` doLayout full viewrect tiled
|
||||||
mapM_ (uncurry tileWindow) rs
|
mapM_ (uncurry tileWindow) rs
|
||||||
|
|
||||||
-- now the floating windows:
|
-- now the floating windows:
|
||||||
@ -388,9 +387,7 @@ instance Message IncMasterN
|
|||||||
-- simple fullscreen mode, just render all windows fullscreen.
|
-- simple fullscreen mode, just render all windows fullscreen.
|
||||||
-- a plea for tuple sections: map . (,sc)
|
-- a plea for tuple sections: map . (,sc)
|
||||||
full :: Layout
|
full :: Layout
|
||||||
full = Layout { doLayout = \sc ws -> return $ case ws of
|
full = Layout { doLayout = \sc (W.Stack f _ _) -> return [(f, sc)]
|
||||||
W.Empty -> []
|
|
||||||
(W.Node f _ _) -> [(f, sc)]
|
|
||||||
, modifyLayout = const (return Nothing) } -- no changes
|
, modifyLayout = const (return Nothing) } -- no changes
|
||||||
|
|
||||||
--
|
--
|
||||||
|
108
StackSet.hs
108
StackSet.hs
@ -74,10 +74,11 @@
|
|||||||
--
|
--
|
||||||
|
|
||||||
module StackSet (
|
module StackSet (
|
||||||
StackSet(..), Workspace(..), Screen(..), Stack(..), RationalRect(..),
|
StackSet(..), Workspace(..), Screen(..), StackOrNot, Stack(..), RationalRect(..),
|
||||||
new, view, lookupWorkspace, peek, index, integrate, differentiate, focusUp, focusDown,
|
new, view, lookupWorkspace, peek, index, integrate, integrate', differentiate,
|
||||||
|
focusUp, focusDown,
|
||||||
focusWindow, member, findIndex, insertUp, delete, shift, filter,
|
focusWindow, member, findIndex, insertUp, delete, shift, filter,
|
||||||
swapMaster, swapUp, swapDown, modify, float, sink -- needed by users
|
swapMaster, swapUp, swapDown, modify, modify', float, sink -- needed by users
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import Prelude hiding (filter)
|
import Prelude hiding (filter)
|
||||||
@ -141,7 +142,7 @@ data Screen i a sid = Screen { workspace :: !(Workspace i a), screen :: !sid }
|
|||||||
-- |
|
-- |
|
||||||
-- A workspace is just a tag - its index - and a stack
|
-- A workspace is just a tag - its index - and a stack
|
||||||
--
|
--
|
||||||
data Workspace i a = Workspace { tag :: !i, stack :: Stack a }
|
data Workspace i a = Workspace { tag :: !i, stack :: StackOrNot a }
|
||||||
deriving (Show, Read, Eq)
|
deriving (Show, Read, Eq)
|
||||||
|
|
||||||
data RationalRect = RationalRect Rational Rational Rational Rational
|
data RationalRect = RationalRect Rational Rational Rational Rational
|
||||||
@ -165,10 +166,11 @@ data RationalRect = RationalRect Rational Rational Rational Rational
|
|||||||
-- structures, it is the differentiation of a [a], and integrating it
|
-- structures, it is the differentiation of a [a], and integrating it
|
||||||
-- back has a natural implementation used in 'index'.
|
-- back has a natural implementation used in 'index'.
|
||||||
--
|
--
|
||||||
data Stack a = Empty
|
type StackOrNot a = Maybe (Stack a)
|
||||||
| Node { focus :: !a -- focused thing in this set
|
|
||||||
, up :: [a] -- clowns to the left
|
data Stack a = Stack { focus :: !a -- focused thing in this set
|
||||||
, down :: [a] } -- jokers to the right
|
, up :: [a] -- clowns to the left
|
||||||
|
, down :: [a] } -- jokers to the right
|
||||||
deriving (Show, Read, Eq)
|
deriving (Show, Read, Eq)
|
||||||
|
|
||||||
|
|
||||||
@ -189,7 +191,7 @@ new :: (Integral i, Integral s) => i -> s -> StackSet i a s
|
|||||||
new n m | n > 0 && m > 0 = StackSet n cur visi unseen M.empty
|
new n m | n > 0 && m > 0 = StackSet n cur visi unseen M.empty
|
||||||
| otherwise = abort "non-positive arguments to StackSet.new"
|
| otherwise = abort "non-positive arguments to StackSet.new"
|
||||||
|
|
||||||
where (seen,unseen) = L.genericSplitAt m $ Workspace 0 Empty : [ Workspace i Empty | i <- [1 ..n-1]]
|
where (seen,unseen) = L.genericSplitAt m $ Workspace 0 Nothing : [ Workspace i Nothing | i <- [1 ..n-1]]
|
||||||
(cur:visi) = [ Screen i s | (i,s) <- zip seen [0..] ]
|
(cur:visi) = [ Screen i s | (i,s) <- zip seen [0..] ]
|
||||||
-- now zip up visibles with their screen id
|
-- now zip up visibles with their screen id
|
||||||
|
|
||||||
@ -232,22 +234,27 @@ lookupWorkspace sc w = listToMaybe [ tag i | Screen i s <- current w : visible w
|
|||||||
|
|
||||||
-- |
|
-- |
|
||||||
-- The 'with' function takes a default value, a function, and a
|
-- The 'with' function takes a default value, a function, and a
|
||||||
-- StackSet. If the current stack is Empty, 'with' returns the
|
-- StackSet. If the current stack is Nothing, 'with' returns the
|
||||||
-- default value. Otherwise, it applies the function to the stack,
|
-- default value. Otherwise, it applies the function to the stack,
|
||||||
-- returning the result. It is like 'maybe' for the focused workspace.
|
-- 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 -> b
|
||||||
with dflt f s = case stack (workspace (current s)) of Empty -> dflt; v -> f v
|
with dflt f = maybe dflt f . stack . workspace . current
|
||||||
-- TODO: ndm: a 'catch' proof here that 'f' only gets Node
|
|
||||||
-- constructors, hence all 'f's are safe below?
|
|
||||||
|
|
||||||
-- |
|
-- |
|
||||||
-- Apply a function, and a default value for Empty, to modify the current stack.
|
-- Apply a function, and a default value for Nothing, to modify the current stack.
|
||||||
--
|
--
|
||||||
modify :: Stack a -> (Stack a -> Stack a) -> StackSet i a s -> StackSet i a s
|
modify :: StackOrNot a -> (Stack a -> StackOrNot a) -> StackSet i a s -> StackSet i a s
|
||||||
modify d f s = s { current = (current s)
|
modify d f s = s { current = (current s)
|
||||||
{ workspace = (workspace (current s)) { stack = with d f s }}}
|
{ workspace = (workspace (current s)) { stack = with d f 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' f = modify Nothing (Just . f)
|
||||||
|
|
||||||
-- |
|
-- |
|
||||||
-- /O(1)/. Extract the focused element of the current stack.
|
-- /O(1)/. Extract the focused element of the current stack.
|
||||||
-- Return Just that element, or Nothing for an empty stack.
|
-- Return Just that element, or Nothing for an empty stack.
|
||||||
@ -259,27 +266,27 @@ peek = with Nothing (return . focus)
|
|||||||
-- /O(n)/. Flatten a Stack into a list.
|
-- /O(n)/. Flatten a Stack into a list.
|
||||||
--
|
--
|
||||||
integrate :: Stack a -> [a]
|
integrate :: Stack a -> [a]
|
||||||
integrate Empty = []
|
integrate (Stack x l r) = reverse l ++ x : r
|
||||||
integrate (Node x l r) = reverse l ++ x : r
|
|
||||||
|
integrate' :: StackOrNot a -> [a]
|
||||||
|
integrate' = maybe [] integrate
|
||||||
|
|
||||||
-- |
|
-- |
|
||||||
-- /O(n)/. Texture a list.
|
-- /O(n)/. Texture a list.
|
||||||
--
|
--
|
||||||
differentiate :: [a] -> Stack a
|
differentiate :: [a] -> StackOrNot a
|
||||||
differentiate [] = Empty
|
differentiate [] = Nothing
|
||||||
differentiate (x:xs) = Node x [] xs
|
differentiate (x:xs) = Just $ Stack x [] xs
|
||||||
|
|
||||||
-- |
|
-- |
|
||||||
-- /O(n)/. 'filter p s' returns the elements of 's' such that 'p' evaluates to
|
-- /O(n)/. 'filter p s' returns the elements of 's' such that 'p' evaluates to
|
||||||
-- True. Order is preserved, and focus moves to the next node to the right (if
|
-- True. Order is preserved, and focus moves to the next node to the right (if
|
||||||
-- necessary).
|
-- necessary).
|
||||||
filter :: (a -> Bool) -> Stack a -> Stack a
|
filter :: (a -> Bool) -> Stack a -> StackOrNot a
|
||||||
filter _ Empty = Empty
|
filter p (Stack f ls rs) = case L.filter p (f:rs) of
|
||||||
filter p (Node f ls rs) = case L.filter p (f:rs) of
|
(f':rs') -> Just $ Stack f' (L.filter p ls) rs'
|
||||||
(f':rs') -> Node f' (L.filter p ls) rs'
|
[] -> do f':rs' <- return $ reverse $ L.filter p ls
|
||||||
[] -> case reverse $ L.filter p ls of
|
Just $ Stack f' [] rs'
|
||||||
[] -> Empty
|
|
||||||
(f':rs') -> Node f' [] rs'
|
|
||||||
|
|
||||||
-- |
|
-- |
|
||||||
-- /O(s)/. Extract the stack on the current workspace, as a list.
|
-- /O(s)/. Extract the stack on the current workspace, as a list.
|
||||||
@ -305,23 +312,22 @@ index = with [] integrate
|
|||||||
-- the current stack.
|
-- the current stack.
|
||||||
--
|
--
|
||||||
focusUp, focusDown, swapUp, swapDown :: StackSet i a s -> StackSet i a s
|
focusUp, focusDown, swapUp, swapDown :: StackSet i a s -> StackSet i a s
|
||||||
focusUp = modify Empty focusUp'
|
focusUp = modify' focusUp'
|
||||||
focusDown = modify Empty (reverseStack . focusUp' . reverseStack)
|
focusDown = modify' (reverseStack . focusUp' . reverseStack)
|
||||||
|
|
||||||
swapUp = modify Empty swapUp'
|
swapUp = modify' swapUp'
|
||||||
swapDown = modify Empty (reverseStack . swapUp' . reverseStack)
|
swapDown = modify' (reverseStack . swapUp' . reverseStack)
|
||||||
|
|
||||||
focusUp', swapUp' :: Stack a -> Stack a
|
focusUp', swapUp' :: Stack a -> Stack a
|
||||||
focusUp' (Node t (l:ls) rs) = Node l ls (t:rs)
|
focusUp' (Stack t (l:ls) rs) = Stack l ls (t:rs)
|
||||||
focusUp' (Node t [] rs) = Node x xs [] where (x:xs) = reverse (t:rs)
|
focusUp' (Stack t [] rs) = Stack x xs [] where (x:xs) = reverse (t:rs)
|
||||||
|
|
||||||
swapUp' (Node t (l:ls) rs) = Node t ls (l:rs)
|
swapUp' (Stack t (l:ls) rs) = Stack t ls (l:rs)
|
||||||
swapUp' (Node t [] rs) = Node t (reverse rs) []
|
swapUp' (Stack t [] rs) = Stack t (reverse rs) []
|
||||||
|
|
||||||
-- | reverse a stack: up becomes down and down becomes up.
|
-- | reverse a stack: up becomes down and down becomes up.
|
||||||
reverseStack :: Stack a -> Stack a
|
reverseStack :: Stack a -> Stack a
|
||||||
reverseStack (Node t ls rs) = Node t rs ls
|
reverseStack (Stack t ls rs) = Stack t rs ls
|
||||||
reverseStack x = x
|
|
||||||
|
|
||||||
--
|
--
|
||||||
-- | /O(1) on current window, O(n) in general/. Focus the window 'w',
|
-- | /O(1) on current window, O(n) in general/. Focus the window 'w',
|
||||||
@ -348,8 +354,8 @@ member a s = maybe False (const True) (findIndex a s)
|
|||||||
findIndex :: Eq a => a -> StackSet i a s -> Maybe i
|
findIndex :: Eq a => a -> StackSet i a s -> Maybe i
|
||||||
findIndex a s = listToMaybe
|
findIndex a s = listToMaybe
|
||||||
[ tag w | w <- workspace (current s) : map workspace (visible s) ++ hidden s, has a (stack w) ]
|
[ tag w | w <- workspace (current s) : map workspace (visible s) ++ hidden s, has a (stack w) ]
|
||||||
where has _ Empty = False
|
where has _ Nothing = False
|
||||||
has x (Node t l r) = x `elem` (t : l ++ r)
|
has x (Just (Stack t l r)) = x `elem` (t : l ++ r)
|
||||||
|
|
||||||
-- ---------------------------------------------------------------------
|
-- ---------------------------------------------------------------------
|
||||||
-- | Modifying the stackset
|
-- | Modifying the stackset
|
||||||
@ -370,10 +376,10 @@ findIndex a s = listToMaybe
|
|||||||
--
|
--
|
||||||
insertUp :: Eq a => a -> StackSet i a s -> StackSet i a s
|
insertUp :: Eq a => a -> StackSet i a s -> StackSet i a s
|
||||||
insertUp a s = if member a s then s else insert
|
insertUp a s = if member a s then s else insert
|
||||||
where insert = modify (Node a [] []) (\(Node t l r) -> Node a l (t:r)) s
|
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 -> StackSet i a s
|
||||||
-- insertDown a = modify (Node a [] []) $ \(Node t l r) -> Node a (t:l) r
|
-- insertDown a = modify (Stack a [] []) $ \(Stack t l r) -> Stack a (t:l) r
|
||||||
-- Old semantics, from Huet.
|
-- Old semantics, from Huet.
|
||||||
-- > w { down = a : down w }
|
-- > w { down = a : down w }
|
||||||
|
|
||||||
@ -381,10 +387,10 @@ insertUp a s = if member a s then s else insert
|
|||||||
-- /O(1) on current window, O(n) in general/. Delete window 'w' if it exists.
|
-- /O(1) on current window, O(n) in general/. Delete window 'w' if it exists.
|
||||||
-- There are 4 cases to consider:
|
-- There are 4 cases to consider:
|
||||||
--
|
--
|
||||||
-- * delete on an Empty workspace leaves it Empty
|
-- * delete on an Nothing workspace leaves it Nothing
|
||||||
-- * otherwise, try to move focus to the down
|
-- * otherwise, try to move focus to the down
|
||||||
-- * otherwise, try to move focus to the up
|
-- * otherwise, try to move focus to the up
|
||||||
-- * otherwise, you've got an empty workspace, becomes Empty
|
-- * otherwise, you've got an empty workspace, becomes Nothing
|
||||||
--
|
--
|
||||||
-- Behaviour with respect to the master:
|
-- Behaviour with respect to the master:
|
||||||
--
|
--
|
||||||
@ -399,13 +405,13 @@ delete w s | Just w == peek s = remove s -- common case.
|
|||||||
removeWindow o n = foldr ($) s [view o,remove,view n]
|
removeWindow o n = foldr ($) s [view o,remove,view n]
|
||||||
|
|
||||||
-- actual removal logic, and focus/master logic:
|
-- actual removal logic, and focus/master logic:
|
||||||
remove = modify Empty $ \c ->
|
remove = modify Nothing $ \c ->
|
||||||
if focus c == w
|
if focus c == w
|
||||||
then case c of
|
then case c of
|
||||||
Node _ ls (r:rs) -> Node r ls rs -- try down first
|
Stack _ ls (r:rs) -> Just $ Stack r ls rs -- try down first
|
||||||
Node _ (l:ls) [] -> Node l ls [] -- else up
|
Stack _ (l:ls) [] -> Just $ Stack l ls [] -- else up
|
||||||
Node _ [] [] -> Empty
|
Stack _ [] [] -> Nothing
|
||||||
else c { up = w `L.delete` up c, down = w `L.delete` down c }
|
else Just $ c { up = w `L.delete` up c, down = w `L.delete` down c }
|
||||||
|
|
||||||
------------------------------------------------------------------------
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
@ -425,9 +431,9 @@ sink w s = s { floating = M.delete w (floating s) }
|
|||||||
-- The old master window is swapped in the tiling order with the focused window.
|
-- The old master window is swapped in the tiling order with the focused window.
|
||||||
-- Focus stays with the item moved.
|
-- Focus stays with the item moved.
|
||||||
swapMaster :: StackSet i a s -> StackSet i a s
|
swapMaster :: StackSet i a s -> StackSet i a s
|
||||||
swapMaster = modify Empty $ \c -> case c of
|
swapMaster = modify' $ \c -> case c of
|
||||||
Node _ [] _ -> c -- already master.
|
Stack _ [] _ -> c -- already master.
|
||||||
Node t ls rs -> Node t [] (ys ++ x : rs) where (x:ys) = reverse ls
|
Stack t ls rs -> Stack t [] (ys ++ x : rs) where (x:ys) = reverse ls
|
||||||
|
|
||||||
-- natural! keep focus, move current to the top, move top to current.
|
-- natural! keep focus, move current to the top, move top to current.
|
||||||
--
|
--
|
||||||
|
@ -16,7 +16,7 @@
|
|||||||
|
|
||||||
module XMonad (
|
module XMonad (
|
||||||
X, WindowSet, WorkspaceId(..), ScreenId(..), XState(..), XConf(..), Layout(..),
|
X, WindowSet, WorkspaceId(..), ScreenId(..), XState(..), XConf(..), Layout(..),
|
||||||
Typeable, Message, SomeMessage(..), fromMessage,
|
Typeable, Message, SomeMessage(..), fromMessage, runLayout,
|
||||||
runX, io, catchIO, withDisplay, withWindowSet, isRoot, spawn, restart, trace, whenJust, whenX,
|
runX, io, catchIO, withDisplay, withWindowSet, isRoot, spawn, restart, trace, whenJust, whenX,
|
||||||
atom_WM_STATE, atom_WM_PROTOCOLS, atom_WM_DELETE_WINDOW
|
atom_WM_STATE, atom_WM_PROTOCOLS, atom_WM_DELETE_WINDOW
|
||||||
) where
|
) where
|
||||||
@ -111,6 +111,9 @@ atom_WM_STATE = getAtom "WM_STATE"
|
|||||||
data Layout = Layout { doLayout :: Rectangle -> Stack Window -> X [(Window, Rectangle)]
|
data Layout = Layout { doLayout :: Rectangle -> Stack Window -> X [(Window, Rectangle)]
|
||||||
, modifyLayout :: SomeMessage -> X (Maybe Layout) }
|
, modifyLayout :: SomeMessage -> X (Maybe Layout) }
|
||||||
|
|
||||||
|
runLayout :: Layout -> Rectangle -> StackOrNot Window -> X [(Window, Rectangle)]
|
||||||
|
runLayout l r = maybe (return []) (doLayout l r)
|
||||||
|
|
||||||
-- Based on ideas in /An Extensible Dynamically-Typed Hierarchy of Exceptions/,
|
-- Based on ideas in /An Extensible Dynamically-Typed Hierarchy of Exceptions/,
|
||||||
-- Simon Marlow, 2006. Use extensible messages to the modifyLayout handler.
|
-- Simon Marlow, 2006. Use extensible messages to the modifyLayout handler.
|
||||||
--
|
--
|
||||||
|
@ -114,7 +114,7 @@ invariant (s :: T) = and
|
|||||||
where
|
where
|
||||||
ws = concat [ focus t : up t ++ down t
|
ws = concat [ focus t : up t ++ down t
|
||||||
| w <- workspace (current s) : map workspace (visible s) ++ hidden s
|
| w <- workspace (current s) : map workspace (visible s) ++ hidden s
|
||||||
, let t = stack w, t /= Empty ] :: [Char]
|
, t <- maybeToList (stack w)] :: [Char]
|
||||||
noDuplicates = nub ws == ws
|
noDuplicates = nub ws == ws
|
||||||
calculatedSize = length (visible s) + length (hidden s) + 1 -- +1 is for current
|
calculatedSize = length (visible s) + length (hidden s) + 1 -- +1 is for current
|
||||||
accurateSize = calculatedSize == size s
|
accurateSize = calculatedSize == size s
|
||||||
@ -148,7 +148,7 @@ prop_focusDown_I (n :: NonNegative Int) (x :: T) =
|
|||||||
prop_focus_I (n :: NonNegative Int) (x :: T) =
|
prop_focus_I (n :: NonNegative Int) (x :: T) =
|
||||||
case peek x of
|
case peek x of
|
||||||
Nothing -> True
|
Nothing -> True
|
||||||
Just _ -> let w = focus . stack . workspace . current $ foldr (const focusUp) x [1..n]
|
Just _ -> let w = focus . fromJust . stack . workspace . current $ foldr (const focusUp) x [1..n]
|
||||||
in invariant $ focusWindow w x
|
in invariant $ focusWindow w x
|
||||||
|
|
||||||
prop_insertUp_I n (x :: T) = invariant $ insertUp n x
|
prop_insertUp_I n (x :: T) = invariant $ insertUp n x
|
||||||
@ -175,7 +175,7 @@ prop_shift_I (n :: NonNegative Int) (x :: T) =
|
|||||||
-- empty StackSets have no windows in them
|
-- empty StackSets have no windows in them
|
||||||
prop_empty (n :: Positive Int)
|
prop_empty (n :: Positive Int)
|
||||||
(m :: Positive Int) =
|
(m :: Positive Int) =
|
||||||
all (== Empty) [ stack w | w <- workspace (current x)
|
all (== Nothing) [ stack w | w <- workspace (current x)
|
||||||
: map workspace (visible x) ++ hidden x ]
|
: map workspace (visible x) ++ hidden x ]
|
||||||
|
|
||||||
where x = new (fromIntegral n) (fromIntegral m) :: T
|
where x = new (fromIntegral n) (fromIntegral m) :: T
|
||||||
@ -257,12 +257,9 @@ prop_member_peek (x :: T) =
|
|||||||
-- the list returned by index should be the same length as the actual
|
-- the list returned by index should be the same length as the actual
|
||||||
-- windows kept in the zipper
|
-- windows kept in the zipper
|
||||||
prop_index_length (x :: T) =
|
prop_index_length (x :: T) =
|
||||||
case it of
|
case stack . workspace . current $ x of
|
||||||
Empty -> length (index x) == 0
|
Nothing -> length (index x) == 0
|
||||||
Node {} -> length (index x) == length list
|
Just it -> length (index x) == length (focus it : up it ++ down it)
|
||||||
where
|
|
||||||
it = stack . workspace . current $ x
|
|
||||||
list = focus it : up it ++ down it
|
|
||||||
|
|
||||||
-- ---------------------------------------------------------------------
|
-- ---------------------------------------------------------------------
|
||||||
-- rotating focus
|
-- rotating focus
|
||||||
@ -293,7 +290,7 @@ prop_focusWindow_works (n :: NonNegative Int) (x :: T) =
|
|||||||
Nothing -> True
|
Nothing -> True
|
||||||
Just _ -> let s = index x
|
Just _ -> let s = index x
|
||||||
i = fromIntegral n `mod` length s
|
i = fromIntegral n `mod` length s
|
||||||
in (focus . stack . workspace . current) (focusWindow (s !! i) x) == (s !! i)
|
in (focus . fromJust . stack . workspace . current) (focusWindow (s !! i) x) == (s !! i)
|
||||||
|
|
||||||
-- rotation through the height of a stack gets us back to the start
|
-- rotation through the height of a stack gets us back to the start
|
||||||
prop_focus_all_l (x :: T) = (foldr (const focusUp) x [1..n]) == x
|
prop_focus_all_l (x :: T) = (foldr (const focusUp) x [1..n]) == x
|
||||||
@ -324,9 +321,8 @@ prop_focusWindow_local (n :: NonNegative Int) (x::T ) =
|
|||||||
prop_findIndex (x :: T) =
|
prop_findIndex (x :: T) =
|
||||||
and [ tag w == fromJust (findIndex i x)
|
and [ tag w == fromJust (findIndex i x)
|
||||||
| w <- workspace (current x) : map workspace (visible x) ++ hidden x
|
| w <- workspace (current x) : map workspace (visible x) ++ hidden x
|
||||||
, let t = stack w
|
, t <- maybeToList (stack w)
|
||||||
, t /= Empty
|
, i <- focus t : up t ++ down t
|
||||||
, i <- focus (stack w) : up (stack w) ++ down (stack w)
|
|
||||||
]
|
]
|
||||||
|
|
||||||
-- ---------------------------------------------------------------------
|
-- ---------------------------------------------------------------------
|
||||||
|
Loading…
x
Reference in New Issue
Block a user