diff --git a/GraphRewriting/GL/Canvas.hs b/GraphRewriting/GL/Canvas.hs
--- a/GraphRewriting/GL/Canvas.hs
+++ b/GraphRewriting/GL/Canvas.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE UnicodeSyntax, FlexibleContexts #-}
 module GraphRewriting.GL.Canvas (setupCanvas) where
 
 import Prelude.Unicode
@@ -5,7 +6,7 @@
 import Graphics.Rendering.OpenGL (($=))
 import GraphRewriting.Graph
 import GraphRewriting.Graph.Read
-import GraphRewriting.Graph.Write.Unsafe as Unsafe
+import qualified GraphRewriting.Graph.Write.Unsafe as Unsafe
 import GraphRewriting.Pattern
 import GraphRewriting.GL.Render
 import GraphRewriting.GL.Global
@@ -13,7 +14,7 @@
 import GraphRewriting.Layout.Rotation
 import GraphRewriting.Layout.Position
 import qualified Data.Set as Set
-import Control.Monad (liftM)
+import Data.Functor
 import Data.Maybe (catMaybes, listToMaybe)
 import Data.Vector.Class
 
@@ -27,7 +28,7 @@
 	aspect ← newIORef 1
 	focus  ← newIORef $ GL.Vector3 0 0 0
 	zoom   ← newIORef (1 ∷ GL.GLdouble)
-	origLayoutStep ← liftM layoutStep $ readIORef globalVars
+	origLayoutStep ← layoutStep <$> readIORef globalVars
 	registerCallbacks origLayoutStep aspect focus zoom project hyperEdgeToLines globalVars
 	GL.cursor $= GL.LeftArrow
 	return canvas
@@ -47,11 +48,19 @@
 
 	inputCallback (GL.MouseButton GL.RightButton) GL.Down mod pos = do
 		pause globalVars
-		rule ← liftM selectedRule $ readIORef globalVars
+		rule ← selectedRule <$> readIORef globalVars
 		node ← nodeAt pos
 		case node of
 			Nothing → return ()
-			Just n  → applyRule (nextIs n rule) globalVars
+			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
 
 	inputCallback (GL.MouseButton GL.RightButton) GL.Up mod (GL.Position x y) = resume globalVars
 
@@ -67,7 +76,7 @@
 					then do
 						pos ← examineNode position node
 						origLayoutStep node
-						updateNode (Position pos) node
+						Unsafe.updateNode node (Position pos)
 					else origLayoutStep node
 				modifyIORef globalVars $ \v → v {layoutStep = fixN}
 				GL.motionCallback $= Just (dragCallback n)
@@ -76,7 +85,7 @@
 			GL.motionCallback $= Nothing
 			GL.Vertex3 tx ty _ ← unproject to
 			let v = Vector2 (convertGLdouble tx) (convertGLdouble ty)
-			modifyGraph (execGraph $ Unsafe.updateNode (Position v) n) globalVars
+			modifyGraph (execGraph $ Unsafe.updateNode n (Position v)) globalVars
 			GL.addTimerCallback 40 $ GL.motionCallback $= Just (dragCallback n)
 
 		scrollCallback from to = do
@@ -84,17 +93,17 @@
 			GL.Vertex3 fx fy _ ← unproject from
 			GL.Vertex3 tx ty _ ← unproject to
 			modifyIORef focus $ \(GL.Vector3 x y _) → GL.Vector3 (x + tx - fx) (y + ty - fy) 0
-			redisplay =<< liftM canvas (readIORef globalVars)
+			redisplay =<< canvas <$> readIORef globalVars
 			GL.addTimerCallback 40 $ GL.motionCallback $= Just (scrollCallback to)
 
 	inputCallback (GL.Char 'z') GL.Up _ _ = autozoom
 	inputCallback (GL.Char ' ') GL.Up _ _ = do
-		isPaused ← liftM paused $ readIORef globalVars
+		isPaused ← paused <$> readIORef globalVars
 		if isPaused then resume globalVars else pause globalVars
 	inputCallback _ _ _ _ = return ()
 
 	autozoom = let margin = 2 in do
-		ns ← liftM (nodes . graph) (readIORef globalVars)
+		ns ← nodes . graph <$> readIORef globalVars
 		let maxDist = maximum $ map abs $ concat [[v2x p, v2y p] | p ← examine position `map` ns]
 		writeIORef focus $ GL.Vector3 0 0 0
 		writeIORef zoom $ 1 / (convertDouble maxDist + margin)
@@ -109,10 +118,13 @@
 		GL.translate =<< readIORef focus
 
 		GL.color (GL.Color3 0 0 0 ∷ GL.Color3 GL.GLfloat)
-		g ← liftM (project . graph) (readIORef globalVars)
+		g ← project . graph <$> readIORef globalVars
 		mapM_ (uncurry renderLine) (concatMap (uncurry hyperEdgeToLines) (edges g))
-		hl ← liftM highlighted (readIORef globalVars)
+		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
 
 		GL.swapBuffers
 
@@ -120,7 +132,7 @@
 	nodeAt glPos = do
 		GL.Vertex3 x y _ ← unproject glPos
 		let pos = Vector2 (convertGLdouble x) (convertGLdouble y)
-		g ← liftM (project . graph) (readIORef globalVars)
+		g ← project . graph <$> readIORef globalVars
 		return $ listToMaybe $ catMaybes $ evalGraph (readOnly $ withNodes $ checkPos pos) g
 		where checkPos pos n = do
 			npos ← examineNode position n
diff --git a/GraphRewriting/GL/Global.hs b/GraphRewriting/GL/Global.hs
--- a/GraphRewriting/GL/Global.hs
+++ b/GraphRewriting/GL/Global.hs
@@ -1,5 +1,7 @@
+{-# LANGUAGE UnicodeSyntax #-}
 module GraphRewriting.GL.Global where
 
+import Prelude.Unicode
 import Graphics.UI.GLUT (addTimerCallback, Window, postRedisplay)
 import GraphRewriting.Graph
 import GraphRewriting.Graph.Read
@@ -7,30 +9,116 @@
 import GraphRewriting.Pattern
 import Data.IORef
 import GraphRewriting.Layout.RotPortSpec
-import Data.Set as Set
-import Data.List ((\\))
-import Control.Monad
+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.Foldable
+import Data.Functor
+import Data.Traversable
+import Prelude hiding (concat, concatMap, or, elem, foldr, any, mapM)
 
+
 data GlobalVars n = GlobalVars
 	{graph        ∷ Graph n,
 	 paused       ∷ Bool,
 	 selectedRule ∷ Rule n,
 	 highlighted  ∷ Set Node,
 	 layoutStep   ∷ Node → Rewrite n (),
-	 canvas       ∷ Window}
+	 canvas       ∷ Window,
+	 menu         ∷ Window,
+	 getRules     ∷ RuleTree n,
+	 selectedIndex ∷ Int}
 
+data LabelledTree a = Branch String [LabelledTree a] | Leaf String a
+
+--data LTZipper a = Root (LabelledTree a) | Child String [LabelledTree a] (LabelledTree 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
+
+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
+
+instance Functor LabelledTree where
+	fmap f (Leaf l x) = Leaf l (f x)
+	fmap f (Branch l ts) = Branch l $ fmap f <$> ts
+
+instance Traversable LabelledTree where
+	traverse f (Leaf l x) = Leaf l <$> f x
+	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
+
+-- 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
+
+-- (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
+
+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
+
+
+-- | 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
+
 redisplay ∷ Window → IO ()
 redisplay = postRedisplay . Just
 
-readGraph = liftM graph . readIORef
+readGraph = fmap graph . readIORef
 writeGraph g = modifyGraph (const g)
 
 modifyGraph f globalVars = do
 	modifyIORef globalVars $ \v → v {graph = f $ graph v}
-	highlight globalVars
+--	highlight globalVars	-- this doesn't work with the command line benchmarking
 
+applyRule ∷ Rule n → IORef (GlobalVars n) → IO ()
 applyRule r globalVars = do
-	layout ← liftM layoutStep $ readIORef globalVars
+	layout ← layoutStep <$> readIORef globalVars
 	g ← readGraph globalVars
 	let ns = evalGraph readNodeList g
 	-- we don't use the fist element of the tuple and compute newNodes ourselves due to a bug in the graph-rewriting package (It's completely out of my hands!!!!1)
@@ -38,6 +126,7 @@
 	let ns' = evalGraph readNodeList g'
 	let newNodes = ns' Data.List.\\ ns
 	writeGraph (execGraph (replicateM_ 15 $ mapM layout newNodes) g') globalVars
+	highlight globalVars
 
 selectRule r globalVars = do
 	modifyIORef globalVars $ \v → v {selectedRule = r}
@@ -62,3 +151,175 @@
 resume globalVars = do
 	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 ()
+
+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
+	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 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
+			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
+
+--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)
+
+--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)
diff --git a/GraphRewriting/GL/HyperEdge.hs b/GraphRewriting/GL/HyperEdge.hs
--- a/GraphRewriting/GL/HyperEdge.hs
+++ b/GraphRewriting/GL/HyperEdge.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE UnicodeSyntax, FlexibleContexts #-}
 module GraphRewriting.GL.HyperEdge where
 
 import GraphRewriting.Graph
diff --git a/GraphRewriting/GL/Menu.hs b/GraphRewriting/GL/Menu.hs
--- a/GraphRewriting/GL/Menu.hs
+++ b/GraphRewriting/GL/Menu.hs
@@ -1,4 +1,4 @@
-module GraphRewriting.GL.Menu (LabeledTree (..), setupMenu) where
+module GraphRewriting.GL.Menu (LabelledTree (..), setupMenu) where
 
 import Prelude.Unicode
 import Graphics.UI.GLUT as GLUT
@@ -10,58 +10,58 @@
 import Control.Monad
 
 
-data LabeledTree a = Branch String [LabeledTree a] | Leaf String a
-
-flattenLT ∷ String → ([a] → a) → LabeledTree 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
-
 menuItemHeight = 20
 font = Fixed9By15
 
-setupMenu ∷ LabeledTree (Rule n) → IORef (GlobalVars n) → IO ()
+setupMenu ∷ LabelledTree (Rule n) → IORef (GlobalVars n) → IO ()
 setupMenu rules globalVars = do
 	c ← liftM canvas $ readIORef globalVars
-	winWidth ← liftM (fromIntegral . maximum) (mapM (stringWidth font) ruleNames)
-	let winSize = Size winWidth (fromIntegral $ menuItemHeight * n)
+	winWidth ← liftM fromIntegral (stringWidth font $ showRuleTree ruleTree)
+	let winSize = Size (winWidth + 60) (fromIntegral $ menuItemHeight * n) -- a little wider to display counters
 	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
-	selectedIndex ← newIORef (0 ∷ Int)
 	selectRule (ruleList !! 0) globalVars
-	displayCallback $= (displayMenu =<< readIORef selectedIndex)
-	keyboardMouseCallback $= Just (inputCallback $ menuClick menu selectedIndex)
+	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 selectedIndex = do
+	displayMenu globalVars = do
+		gv <- readIORef globalVars
 		clear [ColorBuffer]
 		color (Color3 0 0 0 ∷ Color3 GLfloat)
-		zipWithM_ displayLine ruleNames [0..]
+		zipWithM_ displayLine (lines $ showRuleTree ruleTree) [0..]
 		swapBuffers
-		where displayLine name i = do
-			if i ≡ selectedIndex
+		where displayLine line i = do  -- display one line of the menu
+			gv <- readIORef globalVars
+			if i ≡ selectedIndex 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)
-			renderString font name
+			renderString font line
 
 	inputCallback handler (MouseButton button) Up modifiers (Position x y) = do
 		let idx = fromIntegral y `div` menuItemHeight
 		when (0 <= idx ∧ idx < n) (handler button idx)
 	inputCallback _ _ _ _ _ = return ()
 
-	menuClick menu selectedIndex LeftButton idx = do
-		writeIORef selectedIndex idx
+	menuClick menu globalVars LeftButton idx = do
+		modifyIORef globalVars $ \x -> x {selectedIndex = idx}
+		gv <- readIORef globalVars
 		selectRule (ruleList !! idx) globalVars
 		postRedisplay $ Just menu
-	menuClick menu selectedIndex RightButton idx =
-		applyRule (everywhere $ ruleList !! idx) globalVars
+	menuClick menu globalVars RightButton idx = do
+		gv <- readIORef globalVars
+		_ ← applyLeafRules idx globalVars
+		-- TODO: update the resulting subtree
+		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
@@ -4,6 +4,7 @@
 import Data.Vector.V2
 import Graphics.Rendering.OpenGL (GLdouble)
 import qualified Graphics.Rendering.OpenGL as GL
+import qualified Graphics.UI.GLUT as GL
 import Unsafe.Coerce
 
 
@@ -27,3 +28,8 @@
 
 vertex2 ∷ (Double,Double) → IO ()
 vertex2 (x,y) = GL.vertex $ GL.Vertex2 (convertDouble x) (convertDouble y)
+
+renderString label = GL.preservingMatrix $ do
+	GL.translate $ vector2 (-0.3,-0.3)
+	GL.scale 0.007 0.007 (0 ∷ GL.GLdouble)
+	GL.renderString GL.MonoRoman label
diff --git a/GraphRewriting/GL/UI.hs b/GraphRewriting/GL/UI.hs
--- a/GraphRewriting/GL/UI.hs
+++ b/GraphRewriting/GL/UI.hs
@@ -50,22 +50,53 @@
 		 selectedRule = fail "none",
 		 highlighted  = Set.empty,
 		 layoutStep   = \n → layoutStep n >> return (),
-		 canvas       = undefined}
---	print =<< get GL.sampleBuffers
---	print =<< get GL.samples
---	print =<< get GL.subpixelBits
+		 canvas       = undefined,
+		 menu         = undefined,
+		 getRules     = rules,
+		 selectedIndex = 0}
 
---	GL.initialDisplayCapabilities $= [GL.With GL.DisplayDouble, GL.With GL.DisplaySamples]
---	GL.multisample $= GL.Enabled
-	GL.initialDisplayMode $= [GL.DoubleBuffered, GL.Multisampling]
-	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
-	modifyIORef globalVars $ \v → v {canvas = c}
-	setupMenu rules globalVars
-	layoutLoop globalVars
-	GL.mainLoop
-	GL.exit
+
+	-- command line benchmarking
+	file <- case args of
+		("--bench":f:[]) -> do
+			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
+--
+--			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
+	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
+
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.7
+Version:        0.6.9
 Copyright:      (c) 2010, Jan Rochel
 License:        BSD3
 License-File:   LICENSE
@@ -16,10 +16,10 @@
 
 Library
   Build-Depends:
-    base >= 4 && < 4.5,
+    base >= 4 && < 4.6,
     base-unicode-symbols >= 0.2 && < 0.3,
-    graph-rewriting >= 0.4.6 && < 0.6,
-    graph-rewriting-layout >= 0.4 && < 0.5,
+    graph-rewriting >= 0.7 && < 0.8,
+    graph-rewriting-layout >= 0.4 && < 0.6,
     GLUT >= 2.2 && < 2.3,
     OpenGL >= 2.4 && < 2.5,
     containers >= 0.3 && < 0.5,
@@ -38,4 +38,5 @@
     FlexibleContexts
     MultiParamTypeClasses
     TypeSynonymInstances
-  GHC-Options: -fno-warn-duplicate-exports
+    OverlappingInstances
+  GHC-Options:    -fno-warn-duplicate-exports -fwarn-unused-binds -fwarn-unused-imports -fwarn-unused-do-bind -fwarn-wrong-do-bind -fwarn-unrecognised-pragmas