diff --git a/Compressor.hs b/Compressor.hs
deleted file mode 100644
--- a/Compressor.hs
+++ /dev/null
@@ -1,80 +0,0 @@
-{-# language DoAndIfThenElse #-}
-
-import TPDB.Compress (compress)
-import TPDB.DP ( dp, Marked (Auxiliary) )
-import TPDB.Data
-import TPDB.XTC.Read ( readProblems )
-import TPDB.Plain.Write ( )
-import TPDB.Pretty ( pretty )
-import Text.PrettyPrint.HughesPJ 
-  ( text, ($$), nest, vcat )
-
-import System.Environment
-import System.IO
-import System.Directory
-import Control.Monad ( guard, forM )
-import Data.List ( isSuffixOf, isPrefixOf )
-import qualified Data.Set as S
-
--- | give file/dir name(s) on cmd line.
--- recursively collect all *.xml files,
--- and apply TRS compression.
-
-main = do
-    hSetBuffering stdout LineBuffering 
-    args <- getArgs
-    ss <- collect args
-    putStrLn "action"
-    forM ( map dp ss ) $ \ s -> do
-        print $ text "original TRS" </> pretty s 
-        let ( com, rules ) = compress supply s
-        print $ text "compressed TRS" </> vcat
-            ( pretty com : map pretty rules )
-        print $ judge s
-
-p </> q = p $$ nest 4 q
-
-judge sys = 
-    let csys = compress supply sys
-    in  ( cost_trs sys , cost_comp csys )
-
-supply = do 
-    i <- [ 0 .. ] 
-    return $ Auxiliary $ mknullary $ "c" ++ show i
-
-cost_comp ( s, sub ) = 
-    cost_trs s + cost_sub sub
-    
-cost_sub sub = sum $ do
-    ((f, af), Just (g, k, h, ca)) <- sub
-    return ca
-
-cost_trs s = sum $ do
-    u <- rules s
-    t <- [ lhs u, rhs u ]
-    return $ cost_term t
-
-cost_term t = sum $ do 
-    (p,s) <- positions t 
-    return $ multiplications s
-
-multiplications t = case t of
-    Node f xs -> sum $ do
-        x @ Node {} <- xs
-        return $ S.size $ vars x
-    _ -> 0    
-
-collect fs = do
-    let special d = isPrefixOf "." d
-    fss <- forM fs $ \ f -> do
-        d <- doesDirectoryExist f
-        if d 
-        then do
-           fs <- getDirectoryContents f
-           collect $ map ( ( f ++ "/" ) ++ )
-                   $ filter (not . special) fs
-        else if isSuffixOf ".xml" f
-             then fmap (map trs) $ readProblems f
-             else return []
-    return $ concat fss
-
diff --git a/TPDB/CPF/Proof/Type.hs b/TPDB/CPF/Proof/Type.hs
--- a/TPDB/CPF/Proof/Type.hs
+++ b/TPDB/CPF/Proof/Type.hs
@@ -42,7 +42,7 @@
    deriving ( Typeable )
 
 data Sharp i = Sharp i | Plain i
-   deriving ( Typeable )
+   deriving ( Typeable, Eq, Ord )
 
 data DPS = forall s . ( XmlContent s , Typeable s ) 
         => DPS [ Rule (Term Identifier s) ]
diff --git a/TPDB/CPF/Proof/Xml.hs b/TPDB/CPF/Proof/Xml.hs
--- a/TPDB/CPF/Proof/Xml.hs
+++ b/TPDB/CPF/Proof/Xml.hs
@@ -83,6 +83,7 @@
 
 instance XmlContent TrsTerminationProof where
    toContents p = rmkel "trsTerminationProof" $ case p of
+      RIsEmpty -> rmkel "rIsEmpty" []
       DpTrans {} -> rmkel "dpTrans" $
              toContents ( dptrans_dps p )
           ++ rmkel "markedSymbols" [ CString False "true" () ]
diff --git a/TPDB/Compress.hs b/TPDB/Compress.hs
deleted file mode 100644
--- a/TPDB/Compress.hs
+++ /dev/null
@@ -1,179 +0,0 @@
-{-# language TemplateHaskell #-}
-
-module TPDB.Compress where
-
-import TPDB.Data hiding ( trs, arity )
-import TPDB.Plain.Write ()
-import qualified TPDB.Plain.Read (trs) -- for testing
-import TPDB.Pretty 
-
-import Control.Monad ( guard ) 
-import qualified Data.Set as S
-import qualified Data.Map.Strict as M
-import Data.List ( sortBy )
-import Data.Ord ( comparing )
-
-
--- | compute a compressed version of the TRS.
--- Warning: in the output, the arities of fresh identifiers will be nonsensical
-compress :: ( Ord s )
-         => [s] -- ^ supply of function symbols. This can be any infinite list,
-                -- the implementation will filter out those elements that
-                -- occur in the original TRS's signature.
-         -> TRS v s 
-         -> ( TRS v s 
-            , [ ((s, Int), Maybe (s,Int,s,Int) ) ] 
-            ) -- ^  ((f, a), Just (g,i,h,a)) semantics: new function symbols f
-              -- by substituting h in the i-th position (start at 0) of g.
-              -- arity of child is a
-              -- ((f, a), Nothing ) semantics: f of arity a is an "old" function symbol.
-              -- output is in dependency order (will only refer to previously defined symbols).
-compress pool sys = 
-    let osig = ohsig sys
-        forbidden = M.keysSet osig
-        fresh = filter ( `S.notMember` forbidden ) pool
-        con = make fresh sys
-    in  ( trs con 
-        ,    map ( \ fa -> ( fa, Nothing ) ) ( M.toList osig )
-          ++ map ( \ (f, p) -> ( (f, arity p), Just (parent p, branch p, child p, child_arity p) ) ) 
-             (  reverse $ defs con )
-        )
-
-ohsig sys = M.fromListWith ( \ o n -> if o == n then o else error "different arities" ) 
-             $ do u <- rules sys ; t <- [ lhs u , rhs u ]
-                  ( _ , Node f args ) <- positions t
-                  return ( f, length args )
-
-dont_compress pool sys = 
-    let osig = ohsig sys
-    in ( sys , map ( \ fa -> ( fa, Nothing ) ) ( M.toList osig ) )
-                  
-
-data Pattern s = Pattern
-             { parent :: ! s
-             , branch :: ! Int
-             , child :: ! s
-             , arity :: ! Int
-             , child_arity :: ! Int
-             , has_grand_child :: ! Bool 
-             }
-    deriving ( Eq, Ord )
-
-data Container v s = Container 
-               { trs :: TRS v s
-               , defs :: [( s, Pattern s)] 
-               }
-
-make fresh trs = handle fresh $ Container trs []
-
-
-handle free con = 
-    case -- take 1 $ 
-         disjoint $ best_patterns $ trs con of
-        [] -> con
-        ps -> 
-            let ( pre, post ) 
-                    = splitAt ( length ps ) free
-                here = zip pre ps      
-            in handle post
-                 $ con { trs = apply_system here $ trs con
-                       , defs = here ++ defs con
-                       }
-
-patterns_in_term t = 
-    nonoverlapping t ++ overlapping t
-
-overlapping t = do
-    (pos, Node f xs) <- positions t
-    ( k , x @ ( Node g ys ) ) <- zip [ 0 .. ] xs
-    guard $ f == g
-    let sub = case ys !! k of 
-          Node h _ -> True
-          _ -> False
-    guard $ if sub then even $ length pos else True 
-    let r = not $ null $ do Node {} <- ys ; return ()
-    return $ Pattern { arity = length xs - 1 + length ys
-                     , parent = f, branch = k
-                     , child = g, child_arity = length ys
-                     , has_grand_child = r 
-                     }
-
-nonoverlapping t = do
-    Node f xs <- subterms t
-    ( k , x @ ( Node g ys ) ) <- zip [ 0 .. ] xs
-    guard $ f /= g
-    let r = not $ null $ do Node {} <- ys ; return ()
-    return $ Pattern { arity = length xs - 1 + length ys
-                     , parent = f, branch = k
-                     , child = g, child_arity = length ys
-                     , has_grand_child = r 
-                     }
-
-patterns_in_rule u = do
-    t <- [ lhs u, rhs u ]
-    patterns_in_term t
-
-patterns trs = do
-    u <- rules trs
-    patterns_in_rule u
-
-disjoint ps =
-   let h seen [] = []
-       h seen (p:ps) = 
-         if S.notMember (parent p) seen
-            && S.notMember (child p) seen
-         then p : h (S.insert (parent p)   
-                     $ S.insert (child p) seen) ps
-         else h seen ps     
-   in  h S.empty ps 
-
-best_patterns trs = do
-    let pns = sortBy ( comparing ( negate . snd ))
-            $  M.toList $ collect $ patterns trs
-    let threshold = case pns of          
-          [] -> 0
-          (p,n) : _ -> div n 2
-    (p,n) <- takeWhile ( \ (p,n) -> n >= threshold ) pns
-    guard $ ( n > 1 ) || ( n == 1 && has_grand_child p )
-    return p
-
-
-apply_system fgps trs = do
-    trs { rules = map ( apply_rule fgps ) $ rules trs }
-
-apply_rule fgps u = 
-    u { lhs = apply_term fgps $ lhs u
-      , rhs = apply_term fgps $ rhs u
-      }
-
-apply_term _ ( Var v ) = Var v
-apply_term fgps t @ (Node top args) = 
-    let Node newtop newargs = multi_matches fgps t
-    in  Node newtop $ map (apply_term fgps) newargs
-        
-multi_matches [] t = t
-multi_matches ((fg, p@Pattern{parent=f,branch=i,child=g}) : fgps ) t@(Node top args) = 
-    if matches p t
-    then let ( pre, Node _ sub : post) = splitAt i args 
-         in  Node fg ( pre ++ sub ++ post )    
-    else multi_matches fgps t         
-
-matches ( Pattern { parent = f, branch = i, child = g } ) 
-        ( Node top args ) | top == f = 
-    case args !! i of
-         Node bot _ | bot == g -> True
-         _ -> False
-matches p _ = False
-
-
-
-collect xs = M.fromListWith (+) $ do 
-    x <- xs 
-    return ( x, child_arity x )
-
-
-invert :: ( Ord a, Ord b )
-       => M.Map a b -> M.Map b [a]
-invert fm = M.fromListWith (++) $ do
-    ( k, v ) <- M.toList fm
-    return ( v, [k] )
diff --git a/TPDB/Convert.hs b/TPDB/Convert.hs
--- a/TPDB/Convert.hs
+++ b/TPDB/Convert.hs
@@ -9,7 +9,7 @@
               }  
 
 convert_srs_rule u = 
-    let v = Identifier "x" 0 
+    let v = mk 0 "x" 
     in  u { lhs = unspine v $ lhs u
           , rhs = unspine v $ rhs u        
           } 
@@ -28,9 +28,12 @@
 unspine :: v -> [s] -> Term v s
 unspine v = foldr (  \ c t -> Node c [ t ] ) ( Var v )
 
+-- | success iff term consists of unary symbols
+-- and the lowest node is a variable
 spine :: Term v s -> Maybe ( [s], v )
 spine t = case t of
-    Node f [ a ] -> do
-      ( sp, base ) <- spine a 
+    Node f args -> do
+      [ arg ] <- return args
+      ( sp, base ) <- spine arg 
       return ( f : sp, base )
     Var v -> return ( [] , v ) 
diff --git a/TPDB/DP.hs b/TPDB/DP.hs
--- a/TPDB/DP.hs
+++ b/TPDB/DP.hs
@@ -1,19 +1,30 @@
+{-# language OverloadedStrings #-}
+
 module TPDB.DP where
 
 import TPDB.Data
 import TPDB.Pretty
-import Text.PrettyPrint.HughesPJ
+import TPDB.Pretty
 
 import qualified Data.Set as S
 import Control.Monad ( guard )
 
+import Data.Hashable
+import GHC.Generics
+
 data Marked a = Original a | Marked a | Auxiliary a
     deriving ( Eq, Ord )
 
+instance Hashable a => Hashable (Marked a) where
+    hashWithSalt s m = case m of
+        Original x -> hashWithSalt s $ hashWithSalt (0::Int) x
+        Marked x -> hashWithSalt s $ hashWithSalt (1::Int) x
+        Auxiliary x -> hashWithSalt s $ hashWithSalt (2::Int) x
+
 instance Pretty a => Pretty ( Marked a) where
    pretty m = case m of
        Original a -> pretty a
-       Marked a -> pretty a <> text "#"
+       Marked a -> pretty a <> "#"
        Auxiliary a -> pretty a
 
 dp s = 
diff --git a/TPDB/Data.hs b/TPDB/Data.hs
--- a/TPDB/Data.hs
+++ b/TPDB/Data.hs
@@ -14,14 +14,21 @@
 import Data.Typeable
 import Control.Monad ( guard )
 
+import Data.Hashable
 
-data Identifier = Identifier { name :: String , arity :: Int }
+data Identifier = 
+     Identifier { _identifier_hash :: Int
+                , name :: String , arity :: Int }
     deriving ( Eq, Ord, Typeable )
 
+instance Hashable Identifier where
+    hashWithSalt s i = hash (s, _identifier_hash i)
+
 instance Show Identifier where show = name
 
 mk :: Int -> String -> Identifier
-mk a n = Identifier { arity = a, name = n }
+mk a n = Identifier { _identifier_hash = hash (a,n)
+                    , arity = a, name = n }
 
 ---------------------------------------------------------------------
 
diff --git a/TPDB/Input.hs b/TPDB/Input.hs
--- a/TPDB/Input.hs
+++ b/TPDB/Input.hs
@@ -14,28 +14,44 @@
          -> IO ( Either (TRS Identifier Identifier) 
                         ( SRS Identifier ) )
 get f = do
+    m <- getE f
+    case m of
+        Right x -> return x 
+        Left err -> error err
+
+getE f = do
     let ( base, ext ) = splitExtension f    
     case ext of                     
       ".srs" -> do
           s <- readFile f    
           case srs s of
-              Left err -> error err
-              Right t -> return $ Right t
+              Left err -> return $ Left err
+              Right t -> return $ Right $ Right t
       ".trs" -> do        
           s <- readFile f
           case TPDB.Plain.Read.trs s of
-              Left err -> error err
-              Right t -> return $ Left t            
+              Left err -> return $ Left err
+              Right t -> return $ Right $ Left t 
       ".xml" -> do
           ps <- readProblems f
           case ps of 
-              [ p ] -> return $ Left $ TPDB.Data.trs p
+              [ p ] -> return $ Right $ Left $ TPDB.Data.trs p
+              [] -> return $ Left "no TRS"
+              _ -> return $ Left "more than one TRS"
 
 get_trs f = do
     x <- get f
     return $ case x of
         Right x -> srs2trs x
         Left  x -> x
+
+getE_trs f = do
+    e <- getE f
+    return $ case e of
+        Right x -> Right $ case x of
+            Right x -> srs2trs x
+            Left  x -> x
+        Left e -> Left e
 
 get_srs f = do
     x <- get f
diff --git a/TPDB/Plain/Read.hs b/TPDB/Plain/Read.hs
--- a/TPDB/Plain/Read.hs
+++ b/TPDB/Plain/Read.hs
@@ -41,7 +41,7 @@
 instance Reader Identifier where 
     reader = do
         i <- identifier lexer 
-	return $ Identifier { arity = 0 , name = i }
+	return $ mk 0 i
 
 instance Reader s =>  Reader [s] where
     reader = many reader
diff --git a/TPDB/Plain/Write.hs b/TPDB/Plain/Write.hs
--- a/TPDB/Plain/Write.hs
+++ b/TPDB/Plain/Write.hs
@@ -2,17 +2,18 @@
 -- cf. <http://www.lri.fr/~marche/tpdb/format.html>
 
 {-# language FlexibleContexts #-}
+{-# language OverloadedStrings #-}
 
 module TPDB.Plain.Write where
 
 import TPDB.Data
 import TPDB.Pretty
-import Text.PrettyPrint.HughesPJ
 
 import Data.List ( nub )
+import Data.String ( fromString )
 
 instance Pretty Identifier where
-    pretty i = text $ name i
+    pretty i = fromString $ name i
 
 instance ( Pretty v, Pretty s ) => Pretty ( Term v s ) where
     pretty t = case t of
@@ -24,9 +25,9 @@
 instance PrettyTerm a => Pretty ( Rule a ) where
     pretty u = hsep [ prettyTerm $ lhs u
                     , case relation u of 
-                         Strict -> text "->" 
-                         Weak -> text "->="
-                         Equal -> text "="
+                         Strict -> "->" 
+                         Weak -> "->="
+                         Equal -> "="
                     -- FIXME: implement "top" annotation
                     , prettyTerm $ rhs u
                     ]
@@ -42,7 +43,7 @@
 
 instance ( Pretty s, PrettyTerm r ) => Pretty ( RS s r ) where
     pretty sys = vcat 
-        [ parens $ text "RULES" <+>
+        [ parens $ "RULES" <+>
           vcat ( ( if separate sys then punctuate comma else id )
                  $ map pretty $ rules sys 
                )
@@ -57,8 +58,10 @@
        [ pretty $ trs p 
        , case strategy p of  
              Nothing -> empty
-             Just s -> fsep [ text "strategy", text ( show s ) ]
+             Just s -> fsep [ "strategy"
+                            , fromString ( show s ) ]
        , case startterm p of  
              Nothing -> empty
-             Just s -> fsep [ text "startterm", text ( show s ) ]        
+             Just s -> fsep [ "startterm"
+                            , fromString ( show s ) ] 
        ]
diff --git a/TPDB/Pretty.hs b/TPDB/Pretty.hs
--- a/TPDB/Pretty.hs
+++ b/TPDB/Pretty.hs
@@ -1,9 +1,37 @@
-module TPDB.Pretty where
+module TPDB.Pretty 
 
-import Text.PrettyPrint.HughesPJ
+( Doc, SimpleDoc
+, render, renderCompact, displayIO
+, Pretty (..)
+, fsep , hsep, vsep, vcat, hcat
+, parens, brackets, angles, braces, enclose
+, punctuate, comma, nest
+, empty, text
+, (<>), (<+>), ($$)
+)
 
-class Pretty a where pretty :: a -> Doc
+where
 
+import Text.PrettyPrint.Leijen.Text 
+    hiding ( text, (<+>), vcat )
+import qualified Text.PrettyPrint.Leijen.Text 
+import Data.String ( fromString )
+
+-- class Pretty a where pretty :: a -> Doc
+
+fsep = fillSep
+($$) = (<$$>)
+x <+> y = x Text.PrettyPrint.Leijen.Text.<+> align y
+vcat = align . Text.PrettyPrint.Leijen.Text.vcat
+
+render :: Doc -> String
+render = show
+
+text :: String -> Doc
+text = fromString
+
+{-
+
 instance Pretty Int where pretty = text . show
 
 instance ( Pretty a, Pretty b ) => Pretty (a,b) where
@@ -11,10 +39,12 @@
 
 instance ( Pretty a, Pretty b, Pretty c ) => Pretty (a,b,c) where
     pretty (x,y,z) = parens $ fsep $ punctuate comma [ pretty x, pretty y, pretty z ]
+-}
 
 instance ( Pretty a, Pretty b, Pretty c, Pretty d ) => Pretty (a,b,c,d) where
     pretty (x,y,z,u) = parens $ fsep $ punctuate comma [ pretty x, pretty y, pretty z, pretty u ]
 
+{-
 instance Pretty a => Pretty [a]  where
     pretty xs = brackets $ fsep $ punctuate comma $ map pretty xs
 
@@ -22,3 +52,4 @@
     pretty m = case m of
         Nothing -> text "Nothing"
         Just x -> text "Just" <+> pretty x -- FIXME: parens missing
+-}
diff --git a/TPDB/Rainbow/Proof/Type.hs b/TPDB/Rainbow/Proof/Type.hs
--- a/TPDB/Rainbow/Proof/Type.hs
+++ b/TPDB/Rainbow/Proof/Type.hs
@@ -1,4 +1,6 @@
-{-# OPTIONS -fglasgow-exts #-}
+{-# language OverloadedStrings #-}
+{-# language ExistentialQuantification #-}
+{-# language DeriveDataTypeable #-}
 
 -- | internal representation of Rainbow termination proofs,
 -- see <http://color.loria.fr/>
@@ -11,7 +13,6 @@
 import TPDB.Data hiding ( Type (..))
 import TPDB.Pretty
 import TPDB.Plain.Write () -- just instances
-import Text.PrettyPrint.HughesPJ
 
 import qualified TPDB.CPF.Proof.Type as C
 
@@ -20,6 +21,7 @@
 
 import qualified Data.Time as T
 import Data.Typeable
+import Data.String (fromString)
 
 data Vector a = Vector [ a ] 
    deriving Typeable
@@ -64,9 +66,9 @@
 data Domain = Natural | Arctic | Arctic_Below_Zero | Tropical 
     deriving ( Show, Eq, Ord, Typeable )
 
-instance Pretty Domain where pretty = text . show
-instance Pretty T.NominalDiffTime where pretty = text . show
-instance Pretty T.UTCTime where pretty = text . show
+instance Pretty Domain where pretty = fromString . show
+instance Pretty T.NominalDiffTime where pretty = fromString . show
+instance Pretty T.UTCTime where pretty = fromString . show
 
 data Red_Ord 
     = Red_Ord_Matrix_Int Matrix_Int
@@ -79,14 +81,14 @@
     deriving Typeable
 
 instance Pretty Usable_Rules where 
-    pretty (Usable_Rules sp) = text "Usable_Rules" <+> pretty sp
+    pretty (Usable_Rules sp) = "Usable_Rules" <+> pretty sp
 
 
 data Simple_Projection = Simple_Projection [ ( Identifier, Int ) ]
     deriving Typeable
 
 instance Pretty Simple_Projection where 
-    pretty (Simple_Projection sp) = text "Simple_Projection" <+> pretty sp
+    pretty (Simple_Projection sp) = "Simple_Projection" <+> pretty sp
 
 data Claim =
      Claim { system :: TRS Identifier Identifier
@@ -110,9 +112,9 @@
 
 instance Pretty Property where
     pretty p = case p of
-        Termination -> text "YES # Termination"
-        Top_Termination -> text "YES # Top_Termination"
-        Complexity ( lo, hi ) -> text "YES" <+> pretty ( lo, hi ) 
+        Termination -> "YES # Termination"
+        Top_Termination -> "YES # Top_Termination"
+        Complexity ( lo, hi ) -> "YES" <+> pretty ( lo, hi ) 
 
 -- | see specification:
 -- http://termination-portal.org/wiki/Complexity
@@ -126,13 +128,13 @@
 
 instance Pretty Function where
     pretty f = case f of
-        Unknown -> text "?"
+        Unknown -> "?"
         Polynomial { degree = Nothing } -> 
-            text "POLY"
+            "POLY"
         Polynomial { degree = Just 0 } -> 
-            text "O(1)"
+            "O(1)"
         Polynomial { degree = Just d } -> 
-            text "O" <+> parens ( text "n^" <> pretty d)
+            "O" <+> parens ( "n^" <> pretty d)
 
 
 
diff --git a/TPDB/XTC/Read.hs b/TPDB/XTC/Read.hs
--- a/TPDB/XTC/Read.hs
+++ b/TPDB/XTC/Read.hs
@@ -25,13 +25,13 @@
 
 getVar = proc x -> do
     nm <- getText <<< getChildren <<< hasName "var" -< x
-    returnA -< Var $ Identifier { name = nm, arity = 0 }
+    returnA -< Var $ mk 0 nm
 
 getFunApp = proc x -> do
     sub <- hasName "funapp" -< x
     nm <- getText <<< gotoChild "name" -< sub
     gs <- listA ( getTerm <<< gotoChild "arg" ) -< sub
-    let c = Identifier { name = nm, arity = length gs }
+    let c = mk (length gs) nm
     returnA -< Node c gs
           
 gotoChild tag = proc x -> do
@@ -90,7 +90,7 @@
 getFuncsym = proc x -> do
     nm <- getText <<< gotoChild "name" -< x
     ar <- getText <<< gotoChild "arity" -< x
-    returnA -< Identifier { name = nm , arity = read ar }
+    returnA -< mk (read ar) nm
 
 getRules str = proc x -> do
     returnA <<< listA ( getRule str  <<< getChild "rule" ) -< x
diff --git a/TPDB/Xml/Pretty.hs b/TPDB/Xml/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/Xml/Pretty.hs
@@ -0,0 +1,298 @@
+-- | original author: Malcolm Wallace, 
+-- license: LGPL
+-- http://hackage.haskell.org/packages/archive/HaXml/1.23.3/doc/html/Text-XML-HaXml-Pretty.html
+
+-- modified by Johannes Waldmann
+-- to use a different pretty-printer back-end.
+
+-- | This is a pretty-printer for turning the internal representation
+--   of generic structured XML documents into the Doc type (which can
+--   later be rendered using Text.PrettyPrint.HughesPJ.render).
+--   Essentially there is one pp function for each type in
+--   Text.Xml.HaXml.Types, so you can pretty-print as much or as little
+--   of the document as you wish.
+
+{-# language OverloadedStrings #-}
+
+module TPDB.Xml.Pretty
+  (
+  -- * Pretty-print a whole document
+    document
+  -- ** Just one content
+  ,   content
+  -- ** Just one tagged element
+  ,   element
+  -- * Pretty-print just a DTD
+  , doctypedecl
+  -- ** The prolog
+  ,   prolog
+  -- ** A content particle description
+  ,   cp
+  ) where
+
+import Prelude hiding (maybe,either)
+import Data.Maybe hiding (maybe)
+import Data.List (intersperse)
+--import Char (isSpace)
+
+-- import Text.PrettyPrint.HughesPJ
+import TPDB.Pretty hiding ( text )
+
+import Text.XML.HaXml.Types
+import Text.XML.HaXml.Namespaces
+
+import Data.String ( fromString )
+
+text = fromString
+
+either :: (t -> t1) -> (t2 -> t1) -> Either t t2 -> t1
+either f _ (Left x)  = f x
+either _ g (Right x) = g x
+
+maybe :: (t -> Doc) -> Maybe t -> Doc
+maybe _ Nothing  = empty
+maybe f (Just x) = f x
+
+--peref p   = "%" <> text p <> ";"
+
+----
+
+document :: Document i -> Doc
+prolog   :: Prolog -> Doc
+xmldecl  :: XMLDecl -> Doc
+misc     :: Misc -> Doc
+sddecl   :: Bool -> Doc
+
+doctypedecl :: DocTypeDecl -> Doc
+markupdecl  :: MarkupDecl -> Doc
+--extsubset   :: ExtSubset -> Doc
+--extsubsetdecl :: ExtSubsetDecl -> Doc
+cp          :: CP -> Doc
+
+element   :: Element i -> Doc
+attribute :: Attribute -> Doc                     --etc
+content   :: Content i -> Doc
+
+----
+
+document (Document p _ e m)= prolog p $$ element e $$ vcat (map misc m)
+prolog (Prolog x m1 dtd m2)= maybe xmldecl x $$
+                             vcat (map misc m1) $$
+                             maybe doctypedecl dtd $$
+                             vcat (map misc m2)
+xmldecl (XMLDecl v e sd)   = "<?xml version='" <> text v <> "'" <+>
+                             maybe encodingdecl e <+>
+                             maybe sddecl sd <+>
+                             "?>"
+misc (Comment s)           = "<!--" <> text s <> "-->"
+misc (PI (n,s))            = "<?" <> text n <+> text s <> "?>"
+sddecl sd   | sd           = "standalone='yes'"
+            | otherwise    = "standalone='no'"
+doctypedecl (DTD n eid ds) = if null ds then
+                                  hd <> ">"
+                             else hd <+> " [" $$
+                                  vcat (map markupdecl ds) $$ "]>"
+                           where hd = "<!DOCTYPE" <+> qname n <+>
+                                      maybe externalid eid
+markupdecl (Element e)     = elementdecl e
+markupdecl (AttList a)     = attlistdecl a
+markupdecl (Entity e)      = entitydecl e
+markupdecl (Notation n)    = notationdecl n
+markupdecl (MarkupMisc m)  = misc m
+--markupdecl (MarkupPE p m)  = peref p
+
+--extsubset (ExtSubset t ds) = maybe textdecl t $$
+--                             vcat (map extsubsetdecl ds)
+--extmarkupdecl (ExtMarkupDecl m)      = markupdecl m
+--extsubsetdecl (ExtConditionalSect c) = conditionalsect c
+-- -- extsubsetdecl (ExtPEReference p e)   = peref p
+
+element (Elem n as []) = "<" <> qname n <+>
+                         fsep (map attribute as) <> "/>"
+element e@(Elem n as cs)
+    | all isText cs    = "<" <> qname n <+> fsep (map attribute as) <>
+                         ">" <> hcat (map content cs) <>
+                         "</" <> qname n <> ">"
+    | otherwise        = let (d,c) = carryelem e empty
+                         in d <> c
+
+isText :: Content t -> Bool
+isText (CString _ _ _) = True
+isText (CRef _ _)      = True
+isText _               = False
+
+carryelem    ::  Element t  -> Doc -> (Doc, Doc)
+carrycontent ::  Content t  -> Doc -> (Doc, Doc)
+spancontent  :: [Content a] -> Doc -> ([Doc],Doc)
+
+carryelem (Elem n as []) c = ( c <>
+                               "<" <> qname n <+> fsep (map attribute as)
+                             , "/>")
+carryelem (Elem n as cs) c =  let (cs0,d0) = spancontent cs (">") in
+                              ( c <>
+                                "<"<>qname n <+> fsep (map attribute as) $$
+                                nest 2 (vcat cs0) <>
+                                d0 <> "</" <> qname n
+                              , ">")
+
+carrycontent (CElem e _) c         = carryelem e c
+carrycontent (CString False s _) c = (c <> chardata s, empty)
+carrycontent (CString True  s _) c = (c <> cdsect s, empty)
+carrycontent (CRef r _) c          = (c <> reference r, empty)
+carrycontent (CMisc m _) c         = (c <> misc m, empty)
+
+spancontent []     c = ([],c)
+spancontent (a:as) c | isText a  = let (ts,rest) = span isText (a:as)
+                                       formatted = c <> hcat (map content ts)
+                                   in  spancontent rest formatted
+                     | otherwise = let (b, c0) = carrycontent a c
+                                       (bs,c1) = spancontent as c0
+                                   in  (b:bs, c1)
+
+attribute (n,v)             = qname n <> "=" <> attvalue v
+content (CElem e _)         = element e
+content (CString False s _) = chardata s
+content (CString True s _)  = cdsect s
+content (CRef r _)          = reference r
+content (CMisc m _)         = misc m
+
+elementdecl :: ElementDecl -> Doc
+elementdecl (ElementDecl n cs) = "<!ELEMENT" <+> qname n <+>
+                                 contentspec cs <> ">"
+contentspec :: ContentSpec -> Doc
+contentspec EMPTY              = "EMPTY"
+contentspec ANY                = "ANY"
+contentspec (Mixed m)          = mixed m
+contentspec (ContentSpec c)    = cp c
+--contentspec (ContentPE p cs)   = peref p
+cp (TagName n m)       = parens (qname n) <> modifier m
+cp (Choice cs m)       = parens (hcat (intersperse ("|") (map cp cs))) <>
+                           modifier m
+cp (Seq cs m)          = parens (hcat (intersperse (",") (map cp cs))) <>
+                           modifier m
+--cp (CPPE p c)          = peref p
+modifier :: Modifier -> Doc
+modifier None          = empty
+modifier Query         = "?"
+modifier Star          = "*"
+modifier Plus          = "+"
+mixed :: Mixed -> Doc
+mixed  PCDATA          = "(#PCDATA)"
+mixed (PCDATAplus ns)  = "(#PCDATA |" <+>
+                         hcat (intersperse ("|") (map qname ns)) <>
+                         ")*"
+
+attlistdecl :: AttListDecl -> Doc
+attlistdecl (AttListDecl n ds) = "<!ATTLIST" <+> qname n <+>
+                                 fsep (map attdef ds) <> ">"
+attdef :: AttDef -> Doc
+attdef (AttDef n t d)          = qname n <+> atttype t <+> defaultdecl d
+atttype :: AttType -> Doc
+atttype  StringType            = "CDATA"
+atttype (TokenizedType t)      = tokenizedtype t
+atttype (EnumeratedType t)     = enumeratedtype t
+tokenizedtype :: TokenizedType -> Doc
+tokenizedtype ID               = "ID"
+tokenizedtype IDREF            = "IDREF"
+tokenizedtype IDREFS           = "IDREFS"
+tokenizedtype ENTITY           = "ENTITY"
+tokenizedtype ENTITIES         = "ENTITIES"
+tokenizedtype NMTOKEN          = "NMTOKEN"
+tokenizedtype NMTOKENS         = "NMTOKENS"
+enumeratedtype :: EnumeratedType -> Doc
+enumeratedtype (NotationType n)= notationtype n
+enumeratedtype (Enumeration e) = enumeration e
+notationtype :: [String] -> Doc
+notationtype ns                = "NOTATION" <+>
+                                 parens (hcat (intersperse ("|") (map text ns)))
+enumeration :: [String] -> Doc
+enumeration ns                 = parens (hcat (intersperse ("|") (map nmtoken ns)))
+defaultdecl :: DefaultDecl -> Doc
+defaultdecl  REQUIRED          = "#REQUIRED"
+defaultdecl  IMPLIED           = "#IMPLIED"
+defaultdecl (DefaultTo a f)    = maybe (const ("#FIXED")) f <+> attvalue a
+--conditionalsect (IncludeSect i)= "<![INCLUDE [" <+>
+--                                 vcat (map extsubsetdecl i) <+> "]]>"
+--conditionalsect (IgnoreSect i) = "<![IGNORE [" <+>
+--                                 fsep (map ignoresectcontents i) <+> "]]>"
+--ignore (Ignore)                = empty
+--ignoresectcontents (IgnoreSectContents i is)
+--                               = ignore i <+> vcat (map internal is)
+--                          where internal (ics,i) = "<![[" <+>
+--                                                   ignoresectcontents ics <+>
+--                                                   "]]>" <+> ignore i
+reference :: Reference -> Doc
+reference (RefEntity er)       = entityref er
+reference (RefChar cr)         = charref cr
+entityref :: String -> Doc
+entityref n                    = "&" <> text n <> ";"
+charref :: (Show a) => a -> Doc
+charref c                      = "&#" <> text (show c) <> ";"
+entitydecl :: EntityDecl -> Doc
+entitydecl (EntityGEDecl d)    = gedecl d
+entitydecl (EntityPEDecl d)    = pedecl d
+gedecl :: GEDecl -> Doc
+gedecl (GEDecl n ed)           = "<!ENTITY" <+> text n <+> entitydef ed <>
+                                 ">"
+pedecl :: PEDecl -> Doc
+pedecl (PEDecl n pd)           = "<!ENTITY %" <+> text n <+> pedef pd <>
+                                 ">"
+entitydef :: EntityDef -> Doc
+entitydef (DefEntityValue ew)  = entityvalue ew
+entitydef (DefExternalID i nd) = externalid i <+> maybe ndatadecl nd
+pedef :: PEDef -> Doc
+pedef (PEDefEntityValue ew)    = entityvalue ew
+pedef (PEDefExternalID eid)    = externalid eid
+externalid :: ExternalID -> Doc
+externalid (SYSTEM sl)         = "SYSTEM" <+> systemliteral sl
+externalid (PUBLIC i sl)       = "PUBLIC" <+> pubidliteral i <+>
+                                 systemliteral sl
+ndatadecl :: NDataDecl -> Doc
+ndatadecl (NDATA n)            = "NDATA" <+> text n
+--textdecl (TextDecl vi ed)      = "<?xml" <+> maybe text vi <+>
+--                                 encodingdecl ed <+> "?>"
+--extparsedent (ExtParsedEnt t c)= maybe textdecl t <+> content c
+--extpe (ExtPE t esd)            = maybe textdecl t <+>
+--                                 vcat (map extsubsetdecl esd)
+notationdecl :: NotationDecl -> Doc
+notationdecl (NOTATION n e)    = "<!NOTATION" <+> text n <+>
+                                 either externalid publicid e <>
+                                 ">"
+publicid :: PublicID -> Doc
+publicid (PUBLICID p)          = "PUBLIC" <+> pubidliteral p
+encodingdecl :: EncodingDecl -> Doc
+encodingdecl (EncodingDecl s)  = "encoding='" <> text s <> "'"
+nmtoken :: String -> Doc
+nmtoken s                      = text s
+attvalue :: AttValue -> Doc
+attvalue (AttValue esr)        = "\"" <>
+                                 hcat (map (either text reference) esr) <>
+                                 "\""
+entityvalue :: EntityValue -> Doc
+entityvalue (EntityValue evs)
+  | containsDoubleQuote evs    = "'"  <> hcat (map ev evs) <> "'"
+  | otherwise                  = "\"" <> hcat (map ev evs) <> "\""
+ev :: EV -> Doc
+ev (EVString s)                = text s
+--ev (EVPERef p e)               = peref p
+ev (EVRef r)                   = reference r
+pubidliteral :: PubidLiteral -> Doc
+pubidliteral (PubidLiteral s)
+    | '"' `elem` s             = "'" <> text s <> "'"
+    | otherwise                = "\"" <> text s <> "\""
+systemliteral :: SystemLiteral -> Doc
+systemliteral (SystemLiteral s)
+    | '"' `elem` s             = "'" <> text s <> "'"
+    | otherwise                = "\"" <> text s <> "\""
+chardata :: String -> Doc
+chardata s                     = {-if all isSpace s then empty else-} text s
+cdsect :: String -> Doc
+cdsect c                       = "<![CDATA[" <> chardata c <> "]]>"
+
+qname n                        = text (printableName n)
+
+----
+containsDoubleQuote :: [EV] -> Bool
+containsDoubleQuote evs = any csq evs
+    where csq (EVString s) = '"' `elem` s
+          csq _            = False
diff --git a/test/speed.hs b/test/speed.hs
new file mode 100644
--- /dev/null
+++ b/test/speed.hs
@@ -0,0 +1,40 @@
+import Text.XML.HaXml
+
+import qualified Text.XML.HaXml.Pretty as P
+import qualified Text.XML.HaXml.ByteStringPP as BSP
+import qualified Data.ByteString.Lazy.Char8 as BS
+import Text.PrettyPrint.HughesPJ hiding ( int, double )
+
+import qualified TPDB.Pretty as TP
+import qualified TPDB.Xml.Pretty as TXP
+
+import System.IO ( stdout )
+import System.Environment ( getArgs )
+
+mkel name cs = CElem ( Elem (N name) [] cs ) ()
+rmkel name cs = return $ mkel name cs
+
+list xs = foldr ( \ x y -> rmkel "cons" 
+            [ mkel "head" x , mkel "tail" y ] )
+        ( rmkel "nil" [] ) xs
+
+int i = [ CElem (Elem (N "int") 
+    [ (N "val", AttValue [ Left $ show i] ) ] []) () ]
+
+double n = header
+         $ list $ replicate n 
+         $ list $ replicate n $ int 42
+
+header l =
+    let xd = XMLDecl "1.0" 
+             ( Just $ EncodingDecl "UTF-8" ) Nothing 
+        pro = Prolog ( Just xd ) [] Nothing []
+        [ CElem e _ ] =  l
+    in  Document pro emptyST e []
+
+main = do
+    -- print $ P.document
+    -- putStrLn $ renderStyle (Style LeftMode undefined undefined ) $ P.document
+    -- BS.putStrLn $ BSP.document
+    TP.displayIO stdout $ TP.renderCompact $ TXP.document
+            $  double 132
diff --git a/tpdb.cabal b/tpdb.cabal
--- a/tpdb.cabal
+++ b/tpdb.cabal
@@ -1,5 +1,5 @@
 Name: tpdb
-Version: 0.6.1
+Version: 0.7.1
 Author: Johannes Waldmann
 Maintainer: Johannes Waldmann
 Category: Science
@@ -26,38 +26,44 @@
 --   test/3.15.xml, test/33.trs ,  test/z001.srs
 
 Library
-  Build-Depends: base==4.*, hxt, pretty, parsec, time, containers, HaXml, filepath
+  Build-Depends: base==4.*, hxt, wl-pprint-text, 
+    parsec, time, containers, HaXml, filepath, hashable
 
   Exposed-Modules:
     TPDB.Data,     TPDB.Data.Term, TPDB.Data.Xml
-    TPDB.Compress, TPDB.Convert, TPDB.Input
+    -- TPDB.Compress, 
+    TPDB.Convert, TPDB.Input
     TPDB.Mirror, TPDB.DP
     TPDB.Pretty, TPDB.Plain.Write,     TPDB.Plain.Read,
     TPDB.XTC,  TPDB.XTC.Read, TPDB.Xml, 
+    TPDB.Xml.Pretty,
     TPDB.Rainbow.Proof.Xml,     TPDB.Rainbow.Proof.Type
     TPDB.CPF.Proof.Xml,     TPDB.CPF.Proof.Type
 
-Executable Compressor
-    Main-is: Compressor.hs
-    Build-depends: base==4.*, containers >= 0.5, directory, pretty, hxt, parsec
+-- Executable Compressor
+--     Main-is: Compressor.hs
+--    Build-depends: base==4.*, containers >= 0.5, directory, wl-pprint-text, hxt, parsec, hashable
 
 Test-Suite XML
-  Build-Depends: base==4.*, hxt, pretty, parsec, time, containers  >= 0.5, HaXml
+  Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers  >= 0.5, HaXml, hashable
   Type: exitcode-stdio-1.0
   main-is: read_print_xml.hs
   hs-source-dirs: test .
 
 Test-Suite TRS
-  Build-Depends: base==4.*, hxt, pretty, parsec, time, containers  >= 0.5, HaXml
+  Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers  >= 0.5, HaXml, hashable
   Type: exitcode-stdio-1.0
   main-is: read_print_trs.hs
   hs-source-dirs: test .
 
 Test-Suite SRS
-  Build-Depends: base==4.*, hxt, pretty, parsec, time, containers  >= 0.5, HaXml
+  Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers  >= 0.5, HaXml, hashable
   Type: exitcode-stdio-1.0
   main-is: read_print_srs.hs
-
   hs-source-dirs: test .
 
-
+Test-Suite Speed
+  Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers  >= 0.5, HaXml, hashable, pretty,bytestring
+  Type: exitcode-stdio-1.0
+  main-is: speed.hs
+  hs-source-dirs: test .