diff --git a/GraphRewriting/GL/Canvas.hs b/GraphRewriting/GL/Canvas.hs
--- a/GraphRewriting/GL/Canvas.hs
+++ b/GraphRewriting/GL/Canvas.hs
@@ -6,8 +6,8 @@
 import Graphics.Rendering.OpenGL (($=))
 import GraphRewriting.Graph
 import GraphRewriting.Graph.Read
-import qualified GraphRewriting.Graph.Write.Unsafe as Unsafe
 import GraphRewriting.Pattern
+import qualified GraphRewriting.Graph.Write.Unsafe as Unsafe
 import GraphRewriting.GL.Render
 import GraphRewriting.GL.Global
 import Data.IORef
@@ -48,19 +48,12 @@
 
 	inputCallback (GL.MouseButton GL.RightButton) GL.Down mod pos = do
 		pause globalVars
-		rule ← selectedRule <$> readIORef globalVars
 		node ← nodeAt pos
 		case node of
 			Nothing → return ()
 			Just n  → do
-				gv ← readIORef globalVars
-				idx ← getRuleIndex gv (nextIs n rule) (getRules gv)
-				case idx of
-					Nothing -> return ()
-					Just i  -> do
-						let newRuleTree = branchSums $ increaseCounter 0 i 1 (getRules gv)
-						modifyIORef globalVars $ \x -> x {getRules = newRuleTree}
-						applyRule (nextIs n rule) globalVars
+				_ ← (\idx → applyLeafRules (nextIs n) idx globalVars) =<< selectedRule <$> readIORef globalVars
+				highlight globalVars
 
 	inputCallback (GL.MouseButton GL.RightButton) GL.Up mod (GL.Position x y) = resume globalVars
 
@@ -122,9 +115,8 @@
 		mapM_ (uncurry renderLine) (concatMap (uncurry hyperEdgeToLines) (edges g))
 		hl ← highlighted <$> readIORef globalVars
 		mapM_ (renderNode hl) (evalGraph readNodeList g `zip` nodes g)
-		w ← liftM menu $ readIORef globalVars
---		GL.currentWindow $= Just w
-		GL.postRedisplay (Just w) -- redisplay the menu subwindow
+		w ← menu <$> readIORef globalVars
+		redisplay w -- redisplay the menu subwindow
 
 		GL.swapBuffers
 
diff --git a/GraphRewriting/GL/Global.hs b/GraphRewriting/GL/Global.hs
--- a/GraphRewriting/GL/Global.hs
+++ b/GraphRewriting/GL/Global.hs
@@ -11,9 +11,8 @@
 import GraphRewriting.Layout.RotPortSpec
 import qualified Data.Set as Set
 import Data.Set (Set)
-import Data.List ((\\), foldl')
-import Control.Monad (when, replicateM, replicateM_)
-import Data.Monoid
+import Data.List ((\\))
+import Control.Monad (when, replicateM_)
 import Data.Foldable
 import Data.Functor
 import Data.Traversable
@@ -23,32 +22,47 @@
 data GlobalVars n = GlobalVars
 	{graph        ∷ Graph n,
 	 paused       ∷ Bool,
-	 selectedRule ∷ Rule n,
+	 selectedRule ∷ Int,
 	 highlighted  ∷ Set Node,
 	 layoutStep   ∷ Node → Rewrite n (),
 	 canvas       ∷ Window,
 	 menu         ∷ Window,
-	 getRules     ∷ RuleTree n,
-	 selectedIndex ∷ Int}
+	 getRules     ∷ RuleTree n}
 
 data LabelledTree a = Branch String [LabelledTree a] | Leaf String a
 
---data LTZipper a = Root (LabelledTree a) | Child String [LabelledTree a] (LabelledTree a) [LabelledTree a]
+data LTZipper a = Root | Child String [LabelledTree a] (LTZipper a) [LabelledTree a]
 
---forward ∷ LTZipper a → Maybe (LTZipper a)
---forward (Root l) = 
---forward (Child label ls child rs) = case child of
---	Leaf {} → forwardHere
---	Branch label' [    ] → forwardHere
---	Branch label' (t:ts) → 
---	where
---	forwardHere = case rs of
---		[  ] → Nothing
---		r:rs → Just $ Child label (ls ⧺ [child]) r rs
---		[  ] → Nothing
---		r:rs → Just $ Child label (ls ⧺ [child]) r rs
---forward (Child label ls child@(Leaf {}) (r:rs)) = Just $ Child label (ls ⧺ [child]) r rs
+type LTLoc a = (LabelledTree a, LTZipper a)
 
+-- depth-first traversal
+next ∷ LTLoc a → Maybe (LTLoc a)
+next (Branch b (t:ts), p) = Just (t, Child b [] p ts)
+next (Leaf l x, p) = right (Leaf l x, p)
+next _ = Nothing
+
+nth ∷ Int → LTLoc a → Maybe (LTLoc a)
+nth n l = iterate (>>= next) (Just l) !! n
+
+right ∷ LTLoc a → Maybe (LTLoc a)
+right (t, Child c ls p (r:rs)) = Just (r, Child c (ls ⧺ [t]) p rs)
+right (t, Child c ls p []) = up (t, Child c ls p []) >>= right
+right _ = Nothing
+
+up ∷ LTLoc a → Maybe (LTLoc a)
+up (t, Child c ls p rs) = Just (Branch c (ls ⧺ [t] ⧺ rs), p)
+up _ = Nothing
+
+put ∷ LTLoc a → LabelledTree a → LTLoc a
+put (_, p) t = (t, p)
+
+top ∷ LTLoc a → LTLoc a
+top (t, Root) = (t, Root)
+top (t, Child c ls p rs) = top (Branch c (ls ⧺ [t] ⧺ rs), p)
+
+root ∷ LabelledTree a → LTLoc a
+root t = (t, Root)
+
 instance Foldable LabelledTree where
 	foldr f y (Leaf l x) = f x y
 	foldr f y (Branch l ts) = foldr (flip $ foldr f) y ts
@@ -62,49 +76,29 @@
 	traverse f (Branch l ts) = Branch l <$> traverse (traverse f) ts
 
 showRuleTree ∷ RuleTree n → String
-showRuleTree t = show $ fmap (\(n,r) → n) t
---	indentation = 2
---	srt t = case t of
---		Leaf l x    → (x, l ⧺ " " ⧺ show x)
---		Branch l ts → (x, l ⧺ " " ⧺ show x ⧺ concatMap indent lines) where
---			(xs, lines) = unzip $ map srt ts
---			x = mconcat xs
---			indent line = "\n" ⧺ replicate indentation ' ' ⧺ line
-
-instance Show a ⇒ Show (LabelledTree a) where
-	show (Leaf   l x) = l ⧺ " " ⧺ show x
-	show (Branch l s) = l ⧺ " " ⧺ unlines (map (indent . show) s)
-		where indent str = replicate 2 ' ' ⧺ str
+showRuleTree = showLabelledTree 2 0 (+) . fmap fst
 
--- two labeled trees are equal iff their labels and counters are equal
---instance Eq (LabelledTree (Rule n)) where
---	Leaf l1 r1 c1 == Leaf l2 r2 c2 = l1 == l2 && c1 == c2
---	Branch l1 c1 rs1 == Branch l2 c2 rs2 = l1 == l2 && c1 == c2 && and (zipWith (==) rs1 rs2)
---	_ == _ = False
+showLabelledTree ∷ Show a ⇒ Int → a → (a → a → a) → LabelledTree a → String
+showLabelledTree indentation init combine = snd . rec where
 
--- (Pattern n a, [(String, Pattern n a)]) -→ ruleList ∷ [Pattern n a]
---flattenLT ∷ String → ([a] → a) → LabelledTree a → (a,[(String, a)])
---flattenLT indent combine tree = case tree of
---	Leaf l x c → (x,[(l,x)])
---	Branch b c cs → (x, (b,x) : zip (Prelude.map (indent ⧺) strs) ys) where
---		x = combine xs
---		(xs,css) = unzip $ Prelude.map (flattenLT indent combine) cs
---		(strs,ys) = unzip $ concat css
+	rec (Leaf l x) = (x, l ⧺ " " ⧺ show x)
+	rec (Branch l ts) = (x, l ⧺ " " ⧺ show x ⧺ "\n" ⧺ indent (unlines ls)) where
+		x = foldr combine init xs
+		(xs, ls) = unzip $ map rec ts
 
-flattenLT ∷ String → ([a] → a) → LabelledTree a → (a,[(String, a)])
-flattenLT indent combine tree = case tree of
-	Leaf l x → (x,[(l,x)])
-	Branch b cs → (x, (b,x) : zip (map (indent ⧺) strs) ys) where
-		x = combine xs
-		(xs,css) = unzip $ map (flattenLT indent combine) cs
-		(strs,ys) = unzip $ concat css
+	indent str = unlines $ map (replicate indentation ' ' ⧺) (lines str)
 
+	unlines [] = ""
+	unlines [x] = x
+	unlines xs = head xs ⧺ "\n" ⧺ unlines (tail xs)
 
--- | Useful for benchmarking. Print the flattened counters of the rule tree, separated
--- by tabs, so that the numbers can be pasted directly into several cells of a spreadsheet.
-showFlatTabs ∷ Show a ⇒ LabelledTree a → String
-showFlatTabs (Leaf l x)   = show l ⧺ "\t"
-showFlatTabs (Branch l s) = show l ⧺ "\t" ⧺ concatMap showFlatTabs s
+instance Show a ⇒ Show (LabelledTree a) where
+	show (Leaf   l x) = l ⧺ " " ⧺ show x
+	show (Branch l s) = l ⧺ "\n" ⧺ indent (unlines $ map show s) where
+			indent str = unlines $ map (replicate 2 ' ' ⧺) (lines str)
+			unlines [] = ""
+			unlines [x] = x
+			unlines xs = head xs ⧺ "\n" ⧺ unlines (tail xs)
 
 redisplay ∷ Window → IO ()
 redisplay = postRedisplay . Just
@@ -114,7 +108,6 @@
 
 modifyGraph f globalVars = do
 	modifyIORef globalVars $ \v → v {graph = f $ graph v}
---	highlight globalVars	-- this doesn't work with the command line benchmarking
 
 applyRule ∷ Rule n → IORef (GlobalVars n) → IO ()
 applyRule r globalVars = do
@@ -128,12 +121,17 @@
 	writeGraph (execGraph (replicateM_ 15 $ mapM layout newNodes) g') globalVars
 	highlight globalVars
 
-selectRule r globalVars = do
-	modifyIORef globalVars $ \v → v {selectedRule = r}
-	highlight globalVars
+selectRule i globalVars = do
+	ruleListLength ← numNodes <$> getRules <$> readIORef globalVars
+	if 0 ≤ i ∧ i < ruleListLength
+		then do
+			modifyIORef globalVars $ \v → v {selectedRule = i}
+			highlight globalVars
+		else return ()
 
 highlight globalVars = do
-	gv@GlobalVars {graph = g, selectedRule = rule, highlighted = h, canvas = c} ← readIORef globalVars
+	gv@GlobalVars {graph = g, getRules = rs, selectedRule = r, highlighted = h, canvas = c} ← readIORef globalVars
+	let rule = fold $ fmap snd (subtrees rs !! r)
 	let h' = Set.fromList [head match | (match,rewrite) ← runPattern rule g]
 	writeIORef globalVars $ gv {highlighted = h'}
 	redisplay c
@@ -152,174 +150,51 @@
 	modifyIORef globalVars $ \vs → vs {paused = False}
 	layoutLoop globalVars
 
--- | Increases the counter of a Leaf or Branch at the given index by nn
-increaseCounter ∷ Int → Int → Int → LabelledTree (a,Int) → LabelledTree (a,Int)
-increaseCounter = undefined
---increaseCounter i idx nn (Leaf n r c) | i == idx  = Leaf n r (c+nn)
---									  | otherwise = Leaf n r c
---increaseCounter i idx nn (Branch n c rs) | i == idx  = Branch n (c+nn) rs
---									     | otherwise = Branch n c $ increaseCounter' (i+1) idx nn rs
---
---increaseCounter' ∷ Int → Int → Int → [LabelledTree a] → [LabelledTree a]
---increaseCounter' i idx nn [] = []
---increaseCounter' i idx nn (Leaf n r c:rs) | i == idx  = Leaf n r (c+nn) : rs
---									      | otherwise = Leaf n r c : increaseCounter' (i+1) idx nn rs
---increaseCounter' i idx nn (b@(Branch n c rss):rs) | i == idx  = Branch n (c+nn) rss : rs
---											      | otherwise = Branch n c (increaseCounter' (i+1) idx nn rss)
---															  : increaseCounter' (i + nrnodes) idx nn rs
---						where nrnodes = length (flattenedLT b)
-
 subtrees ∷ LabelledTree a → [LabelledTree a]
 subtrees t = t : case t of
 	Leaf _ _ → []
 	Branch l ts → concatMap subtrees ts
 
---subtree' i (Branch l s) = 
---subtree' i (l@(Leaf n r c):rs) | i == idx  = Right l
---								   | otherwise = subtree' (i+1) idx rs
---subtree' i idx (b@(Branch n c rss):rs) | i == idx  = Right b
---									   | otherwise = case subtree' (i+1) idx rss of
---											Left i  → subtree' i idx rs -- we already increased i earlier here
---											Right t → Right t
-
--- | Given a list of matches (i.e. [[Node]]) it will pick all matches if none of
--- its nodes has been picked before
-filterOverlaps ∷ [Match] → Set Match
-filterOverlaps = Set.fromList . snd . foldr add (Set.empty, []) where
-	add m (ns, ms) = if any (`Set.member` ns) m then (ns, ms) else (foldr Set.insert ns m, m:ms)
-
---applyLeafRule ∷ Int → [Match] → IORef (GlobalVars n) → LabelledTree (Rule n) → IO ()
---applyLeafRule idx ms gvs (Leaf n r c) = do
---	gv ← readIORef gvs
---	layout ← liftM layoutStep $ readIORef gvs
---	g ← readGraph gvs
---	let ns = evalGraph readNodeList g
---	let redexes = head $ evalPattern (amnesia $ matches r) (graph gv)
---	    nonOverlappingMatches = [m | m ← filterOverlaps redexes, m `elem` ms]
---	    nrMatched = length nonOverlappingMatches
---	    newRuleTree = branchSums $ increaseCounter 0 idx nrMatched (getRules gv)
---	    g' = execGraph (apply $ exhaustive $ restrictOverlap (\past future → future `elem` nonOverlappingMatches) r) g
---	modifyIORef gvs $ \x → x {getRules = newRuleTree}
---	let ns' = evalGraph readNodeList g'
---	let newNodes = ns' Data.List.\\ ns
---	writeGraph (execGraph (replicateM_ 15 $ mapM layout newNodes) g') gvs
---applyLeafRule idx ms gvs (Branch n c rs) = return ()
+numNodes ∷ LabelledTree a → Int
+numNodes = length . subtrees
 
 type RuleTree n = LabelledTree (Int, Rule n)
 
 -- | Traverses the rule tree depth-first and executes all leaf rules it encounters. Rules are
 -- executed everywhere they match, except if they overlap one of them is chosen at random.
 -- So this corresponds to a complete development.
-applyLeafRules ∷ Int → IORef (GlobalVars n) → IO ()
-applyLeafRules idx gvs = do
+applyLeafRules ∷ (Rule n → Rule n) → Int → IORef (GlobalVars n) → IO ()
+applyLeafRules restriction idx gvs = do
 	g ← readGraph gvs
 	comptree ← getRules <$> readIORef gvs
-	let trees = subtrees comptree
-	if not $ 0 ≤ idx ∧ idx < length trees
-		then return ()
-		else do
-			let tree = trees !! idx
+	let pos = nth idx (root comptree)
+	case pos of
+		Nothing → return ()
+		Just (tree,p) → do
 			let ns = evalGraph readNodeList g
-			let rule = fold $ fmap snd tree
-			let nonOverlappingMatches = filterOverlaps $ head $ evalPattern (matches rule) g
-			let ((_, g'), tree') = mapAccumR applyLeafRules' (nonOverlappingMatches, g) tree
+			-- first we mark all redexes
+			let rule = restriction $ fold $ fmap snd tree
+			-- then we find a non-overlapping subset
+			let ms = head $ evalPattern (matches rule) g
+			-- then we apply the rules in the leafs while restricting them to that subset
+			let ((_, g'), tree') = mapAccumL applyLeafRules' (ms, g) tree
 			let ns' = evalGraph readNodeList g'
 			let newNodes = ns' Data.List.\\ ns
 			layout ← layoutStep <$> readIORef gvs
 			writeGraph (execGraph (replicateM_ 15 (mapM layout newNodes)) g') gvs
-			modifyIORef gvs $ \x → x {getRules = insertTree idx tree tree'}
-
-insertTree ∷ Int → LabelledTree a → LabelledTree a → LabelledTree a
-insertTree pos tree tree' = tree
---insertTree pos subtree tree = case insert' pos tree of
---	Left pos' → tree
---	Right res → res
---	where
---	insert' 0 t = Right subtree
---	insert' p t = case t of
---		Leaf l x → Left (p+1)
---		Branch l [] → Left p
---		Branch l ts → case muh ts (Left p) of
---			Left p' → Left p'
---			Right ts' → Right $ Branch l ts'
---			where
---			muh ∷ [LabelledTree a] → Either Int [LabelledTree a] → Either Int [LabelledTree a]
---			muh [] (Left p) = Left p
---			muh (t:ts) (Left p) = case insert' p t of
---				Left p' → 
---				Right t' → Right $ t'
---			muh t (Left p) = insert' p t
-
--- At every leaf apply the rule restricted to the set of predetermined matches, every time removing the
--- the match from the set updating the graph and the counter.
-applyLeafRules' ∷ (Set Match, Graph n) → (Int, Rule n) → ((Set Match, Graph n), (Int, Rule n))
-applyLeafRules' (matches, g) (n, r) = let
-		ms = runPattern r' g
-		r' = restrictOverlap (\past future → future `elem` matches) r
-	in if null ms
-		then ((matches, g), (n, r))
-		else let
-				(match, rewrite) = head ms
-				g' = execGraph rewrite g
-			in applyLeafRules' (Set.delete match matches, g') (n+1, r)
-
---applyLeafRules' idx ms gvs (l@(Leaf n r c):rs) = do
---	applyLeafRule idx ms gvs l
---	applyLeafRules' (idx+1) ms gvs rs
---applyLeafRules' idx ms gvs (b@(Branch n c rss):rs) = do
---	selIdx ← applyLeafRules' (idx+1) ms gvs rss -- get the last index in a subtree
---	applyLeafRules' selIdx ms gvs rs
---applyLeafRules' idx ms gvs [] = return idx
-
--- | Flattens the LabelledTree into a list of its nodes, where the branch nodes have
--- empty lists attached to them
---flattenedLT ∷ LabelledTree a → [LabelledTree a]
---flattenedLT l@(Leaf n r c)  = [l]
---flattenedLT (Branch n c rs) = Branch n c [] : concatMap flattenedLT rs
-
---branchSums ∷ LabelledTree a → LabelledTree a
---branchSums l@(Leaf n r c)  = l
---branchSums (Branch n c rs) = Branch n (sum $ childCounters rs) (Prelude.map branchSums rs)
-
---childCounters ∷ [LabelledTree a] → [Int]
---childCounters [] = []
---childCounters ((Leaf n r c):rs)     = c : childCounters rs
---childCounters ((Branch n c rss):rs) = sum (childCounters rss) : childCounters rs
-
--- | Looks up the index of a given leaf rule in the rule tree.
---getRuleIndex ∷ GlobalVars n → Rule n → LabelledTree (Rule n) → IO (Maybe Int)
---getRuleIndex gvs rl l = getRuleIndex' 0 gvs rl l
+			modifyIORef gvs $ \x → x {getRules = fst $ top (tree',p)}
 
---getRuleIndex' ∷ Int → GlobalVars n → Rule n → LabelledTree (Rule n) → IO (Maybe Int)
---getRuleIndex' idx gvs rl (Leaf n r c)     = do
---	let rlMatches = getMatches rl gvs
---	    rMatches  = getMatches r gvs
---	if Prelude.null rlMatches
---		then return Nothing
---		else if head rlMatches `elem` rMatches
---				then return (Just idx)
---				else return Nothing
---getRuleIndex' idx gvs rl (Branch n c rs) = do
---	selIdx ← getRuleIndex'' (idx+1) gvs rl rs
---	case selIdx of
---		Left _  → return Nothing
---		Right i → return (Just i)
+	where
 
---getRuleIndex'' ∷ Int → GlobalVars n → Rule n → [LabelledTree (Rule n)] → IO (Either Int Int)
---getRuleIndex'' idx gvs rl [] = return (Left idx)
---getRuleIndex'' idx gvs rl ((Leaf n r c):rs)     = do
---	let rlMatches = getMatches rl gvs
---	    rMatches  = getMatches r gvs
---	if Prelude.null rlMatches
---		then return (Left idx)
---		else if head rlMatches `elem` rMatches
---				then return (Right idx)
---				else getRuleIndex'' (idx+1) gvs rl rs
---getRuleIndex'' idx gvs rl ((Branch n c rss):rs) = do
---	selIdx ← getRuleIndex'' (idx+1) gvs rl rss
---	case selIdx of
---		Left i  → getRuleIndex'' i gvs rl rs
---		Right i → return (Right i)
---
---getMatches ∷ Rule n → GlobalVars n → [Match]
---getMatches r gvs = Prelude.map fst $ snd $ head $ runPattern (amnesia $ match r) (graph gvs)
+	-- At every leaf apply the rule restricted to the set of predetermined matches, every time removing the
+	-- the match from the set updating the graph and the counter.
+--	applyLeafRules' ∷ ([Match], Graph n) → (Int, Rule n) → (([Match], Graph n), (Int, Rule n))
+	applyLeafRules' (matches, g) (n, r) = let
+			ms = runPattern r' g
+			r' = restrictOverlap (\past future → future `elem` matches) (restriction r)
+		in if null ms
+			then ((matches, g), (n, r))
+			else let
+					(match, rewrite) = head ms
+					g' = execGraph rewrite g
+				in applyLeafRules' (filter (\m → not $ any (`elem` match) m) matches, g') (n + 1, r)
diff --git a/GraphRewriting/GL/Menu.hs b/GraphRewriting/GL/Menu.hs
--- a/GraphRewriting/GL/Menu.hs
+++ b/GraphRewriting/GL/Menu.hs
@@ -4,64 +4,60 @@
 import Graphics.UI.GLUT as GLUT
 import qualified Graphics.Rendering.OpenGL as GL
 import GraphRewriting.GL.Global
-import GraphRewriting.Rule
 import Data.IORef
-import GraphRewriting.Pattern
 import Control.Monad
+import Data.Functor
+import Control.Applicative
 
 
 menuItemHeight = 20
 font = Fixed9By15
 
-setupMenu ∷ LabelledTree (Rule n) → IORef (GlobalVars n) → IO ()
-setupMenu rules globalVars = do
+setupMenu ∷ IORef (GlobalVars n) → IO ()
+setupMenu globalVars = do
 	c ← liftM canvas $ readIORef globalVars
-	winWidth ← liftM fromIntegral (stringWidth font $ showRuleTree ruleTree)
-	let winSize = Size (winWidth + 60) (fromIntegral $ menuItemHeight * n) -- a little wider to display counters
+	ruleTree ← getRules <$> readIORef globalVars
+	winWidth ← liftM fromIntegral <$> (+) <$> (stringWidth font $ showRuleTree ruleTree) <*> stringWidth font "0"
+	let ruleListLength = numNodes ruleTree
+	let winSize = Size winWidth (fromIntegral $ menuItemHeight * ruleListLength)
 	menu ← createSubWindow c (GL.Position 0 0) winSize
 	modifyIORef globalVars $ \x -> x {menu=menu} -- set the menu subwindow
 	clearColor $= (Color4 1 1 1 0 ∷ Color4 GLclampf)
 
 	GLUT.cursor $= GLUT.LeftArrow
-	selectRule (ruleList !! 0) globalVars
+	selectRule 0 globalVars
 	displayCallback $= displayMenu globalVars
 	keyboardMouseCallback $= Just (inputCallback $ menuClick menu globalVars)
 	where
 
-	ruleTree = fmap (\r → (0,r)) rules
-
-	(ruleNames, ruleList) = unzip $ snd $ flattenLT "   " anyOf rules
-	n = length ruleNames
-
 	displayMenu globalVars = do
 		gv <- readIORef globalVars
 		clear [ColorBuffer]
 		color (Color3 0 0 0 ∷ Color3 GLfloat)
-		zipWithM_ displayLine (lines $ showRuleTree ruleTree) [0..]
-		swapBuffers
-		where displayLine line i = do  -- display one line of the menu
+		ruleTree ← getRules <$> readIORef globalVars
+		let ruleListLength = numNodes ruleTree
+		let displayLine line i = do  -- display one line of the menu
 			gv <- readIORef globalVars
-			if i ≡ selectedIndex gv
+			if i ≡ selectedRule gv
 				then GL.color (GL.Color3 1 0 0 ∷ GL.Color3 GL.GLfloat)
 				else GL.color (GL.Color3 0 0 0 ∷ GL.Color3 GL.GLfloat)
-			windowPos (Vertex2 0 (fromIntegral $ (n - i - 1) * menuItemHeight + 5) ∷ Vertex2 GLint)
+			windowPos (Vertex2 0 (fromIntegral $ (ruleListLength - i - 1) * menuItemHeight + 5) ∷ Vertex2 GLint)
 			renderString font line
+		zipWithM_ displayLine (lines $ showRuleTree ruleTree) [0..]
+		swapBuffers
 
 	inputCallback handler (MouseButton button) Up modifiers (Position x y) = do
 		let idx = fromIntegral y `div` menuItemHeight
-		when (0 <= idx ∧ idx < n) (handler button idx)
+		handler button idx
 	inputCallback _ _ _ _ _ = return ()
 
 	menuClick menu globalVars LeftButton idx = do
-		modifyIORef globalVars $ \x -> x {selectedIndex = idx}
+		modifyIORef globalVars $ \x -> x {selectedRule = idx}
 		gv <- readIORef globalVars
-		selectRule (ruleList !! idx) globalVars
-		postRedisplay $ Just menu
+		selectRule idx globalVars
+		redisplay menu
 	menuClick menu globalVars RightButton idx = do
 		gv <- readIORef globalVars
-		_ ← applyLeafRules idx globalVars
-		-- TODO: update the resulting subtree
+		_ ← applyLeafRules id idx globalVars
 		highlight globalVars
---		applyRule (everywhere $ ruleList !! idx) globalVars
-		postRedisplay $ Just menu
 	menuClick _ _ _ _  = return ()
diff --git a/GraphRewriting/GL/Render.hs b/GraphRewriting/GL/Render.hs
--- a/GraphRewriting/GL/Render.hs
+++ b/GraphRewriting/GL/Render.hs
@@ -29,6 +29,7 @@
 vertex2 ∷ (Double,Double) → IO ()
 vertex2 (x,y) = GL.vertex $ GL.Vertex2 (convertDouble x) (convertDouble y)
 
+renderString ∷ String → IO ()
 renderString label = GL.preservingMatrix $ do
 	GL.translate $ vector2 (-0.3,-0.3)
 	GL.scale 0.007 0.007 (0 ∷ GL.GLdouble)
diff --git a/GraphRewriting/GL/UI.hs b/GraphRewriting/GL/UI.hs
--- a/GraphRewriting/GL/UI.hs
+++ b/GraphRewriting/GL/UI.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE UnicodeSyntax, FlexibleContexts #-}
 -- | This module provides an easy-to-use interface to create an interactive, graphical front-end for you graph rewriting system. The controls of the GUI are as follows:
 --
 -- - Left-click on a menu entry to /select/ a rewriting rule. At all times all redexes with respect to the selected rule are marked red in the graph. Note that the menu is hierarchical, which means that selecting a rule that has subordinate entries has the effect of all these entries being selected.
@@ -15,7 +16,7 @@
 -- - Press space to pause/resume layouting. Currently layouting is automatically resumed when the graph is rewritten by right-clicking on an individual node and not when right-clicking on a menu entry. This also requires the mouse cursor to be positioned in the canvas area.
 --
 -- Please have a look the graph-rewriting-ski package for an example application that makes use of this library.
-module GraphRewriting.GL.UI (module GraphRewriting.GL.UI, LabeledTree (..)) where
+module GraphRewriting.GL.UI (module GraphRewriting.GL.UI, LabelledTree (..)) where
 
 import qualified Graphics.UI.GLUT as GL
 import Graphics.UI.GLUT (($=), get)
@@ -41,62 +42,53 @@
     → (Graph n → Graph n') -- ^ A projection function that is applied just before displaying the graph
     → (Node → Rewrite n a) -- ^ The monadic graph transformation code for a layout step
     → Graph n
-    → LabeledTree (Rule n) -- ^ The rule menu given as a tree of named rules
+    → LabelledTree (Rule n) -- ^ The rule menu given as a tree of named rules
     → IO ()
 run initSteps project layoutStep g rules = do
 	globalVars ← newIORef $ GlobalVars
 		{graph        = execGraph (replicateM_ initSteps $ mapM layoutStep =<< readNodeList) g,
 		 paused       = False,
-		 selectedRule = fail "none",
+		 selectedRule = 0,
 		 highlighted  = Set.empty,
 		 layoutStep   = \n → layoutStep n >> return (),
 		 canvas       = undefined,
 		 menu         = undefined,
-		 getRules     = rules,
-		 selectedIndex = 0}
+		 getRules     = fmap (\r → (0,r)) rules}
 
 
 	-- command line benchmarking
-	file <- case args of
-		("--bench":f:[]) -> do
-			gvs <- readIORef globalVars
-			finalTree <- reduceAll globalVars (graph gvs) rules
+--			gvs <- readIORef globalVars
+--			finalTree <- reduceAll globalVars (graph gvs) rules
 --			putStrLn ("Nr of reductions to normal form:\n" ++ showIndent 0 finalTree) -- (getTopCounter finalTree))
-			putStrLn $ showFlatTabs finalTree
-		_ -> do
-			GL.initialDisplayMode $= [GL.DoubleBuffered, GL.Multisampling]
---			print =<< get GL.sampleBuffers
---			print =<< get GL.samples
---			print =<< get GL.subpixelBits
+--			putStrLn $ showFlatTabs finalTree
+	GL.initialDisplayMode $= [GL.DoubleBuffered, GL.Multisampling]
+--	print =<< get GL.sampleBuffers
+--	print =<< get GL.samples
+--	print =<< get GL.subpixelBits
 --
---			GL.initialDisplayCapabilities $= [GL.With GL.DisplayDouble, GL.With GL.DisplaySamples]
---			GL.multisample $= GL.Enabled
-			p ← get GL.displayModePossible
-			when (not p) $ do
-				GL.initialDisplayMode $= [GL.DoubleBuffered]
-				p ← get GL.displayModePossible
-				when (not p) $ GL.initialDisplayMode $= []
-			c ← setupCanvas project star globalVars    -- creates the window, registers callbacks
-			modifyIORef globalVars $ \v → v {canvas = c}
-			setupMenu rules globalVars
-			layoutLoop globalVars
-			GL.mainLoop
-			GL.exit
+--	GL.initialDisplayCapabilities $= [GL.With GL.DisplayDouble, GL.With GL.DisplaySamples]
+--	GL.multisample $= GL.Enabled
+	p ← get GL.displayModePossible
+	when (not p) $ do
+		GL.initialDisplayMode $= [GL.DoubleBuffered]
+		p ← get GL.displayModePossible
+		when (not p) $ GL.initialDisplayMode $= []
+	c ← setupCanvas project star globalVars    -- creates the window, registers callbacks
+	modifyIORef globalVars $ \v → v {canvas = c}
+	setupMenu globalVars
+	layoutLoop globalVars
+	GL.mainLoop
+	GL.exit
 	return ()
 
-reduceAll :: IORef (GlobalVars n) -> Graph n -> LabeledTree (Rule n) -> IO (LabeledTree (Rule n))
-reduceAll globalVars g ruleTree = do
-	let ns = evalGraph readNodeList g
-	applyLeafRules 0 globalVars ruleTree
-	gvs <- readIORef globalVars
-	let g' = graph gvs
-	    ruleTree' = getRules gvs
-	    ns' = evalGraph readNodeList g'
-	if  ruleTree == ruleTree'
-		then return ruleTree'
-		else reduceAll globalVars g' ruleTree'
-
-getTopCounter :: LabeledTree (Rule n) -> Int
-getTopCounter (Leaf n r c)    = c
-getTopCounter (Branch n c rs) = c
-
+--reduceAll :: IORef (GlobalVars n) -> Graph n -> RuleTree n -> IO (RuleTree n)
+--reduceAll globalVars g ruleTree = do
+--	let ns = evalGraph readNodeList g
+--	applyLeafRules 0 globalVars
+--	gvs <- readIORef globalVars
+--	let g' = graph gvs
+--	    ruleTree' = getRules gvs
+--	    ns' = evalGraph readNodeList g'
+--	if ruleTree == ruleTree'
+--		then return ruleTree'
+--		else reduceAll globalVars g' ruleTree'
diff --git a/graph-rewriting-gl.cabal b/graph-rewriting-gl.cabal
--- a/graph-rewriting-gl.cabal
+++ b/graph-rewriting-gl.cabal
@@ -1,5 +1,5 @@
 Name:           graph-rewriting-gl
-Version:        0.6.9
+Version:        0.7
 Copyright:      (c) 2010, Jan Rochel
 License:        BSD3
 License-File:   LICENSE