diff --git a/AgdaHighlight.hs b/AgdaHighlight.hs
deleted file mode 100644
--- a/AgdaHighlight.hs
+++ /dev/null
@@ -1,120 +0,0 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-
-module AgdaHighlight
-    ( highlightAgdaAsXHtml
---    , FormatOption (..)
-    ) where
-
-import Text.Highlighting.Kate as Kate
-import Text.Blaze.Renderer.String
-
-import Control.Monad.State
-import System.IO.Unsafe
-
-import Agda.Syntax.Literal
-import Agda.Syntax.Position
-import Agda.Syntax.Parser
-import Agda.Syntax.Parser.Tokens (Token(..))
-
-highlightAgdaAsXHtml :: String -> String
-highlightAgdaAsXHtml code = formattedCode
-    where
-        language              = "agda"
-        (Right highlightInfo) = highlight code
-        formattedCode         = renderHtml $ formatHtmlBlock defaultFormatOpts highlightInfo
-
--- | Highlight source code using this syntax definition.
-highlight :: String -> Either String [SourceLine]
-highlight input = Right $ runSourceLineGen $ do
-  tokens <- liftIO $ parse tokensParser input
-  -- tokens :: IO [Tokens]
-  -- Other parsing method needed - or unsafePerformIO
-  -- map tokenToSourceLine tokens
-  mapM_ processToken tokens
-  where
---    processToken :: Token -> SourceLineGen ()
-    processToken token =
-        case token of
-            TokKeyword kw iv     -> addByInterval (KeywordTok, getSourceByInterval iv) iv -- kw
-            TokId (iv, id)       -> addByInterval (DataTypeTok, getSourceByInterval iv) iv -- dt
-            TokQId ivds          -> mapM_ (\(iv, id) -> addByInterval (DataTypeTok, getSourceByInterval iv) iv) ivds -- dt
-            TokLiteral lit       ->
-                case lit of
-                    LitInt r i      -> addByRange (DecValTok,  getSourceByRange r) r -- dv
-                    LitFloat r d    -> addByRange (FloatTok,   getSourceByRange r) r -- fl
-                    LitString r str -> addByRange (StringTok,  getSourceByRange r) r -- st
-                    LitChar r ch    -> addByRange (CharTok,    getSourceByRange r) r -- ch
-                    LitQName r qn   -> addByRange (OtherTok,   getSourceByRange r) r -- ?
-            TokSymbol sym iv     -> addByInterval (FunctionTok, getSourceByInterval iv) iv -- TODO: switch by symbol?
-            TokString (iv, str)  -> addByInterval (StringTok,  getSourceByInterval iv) iv -- st
-            TokSetN (iv, n)      -> addByInterval (OtherTok,   "TokSetN") iv   -- ?
-            TokTeX (iv, str)     -> addByInterval (OtherTok,   "TokTex") iv    -- ?
-            TokComment (iv, str) -> addByInterval (CommentTok, getSourceByInterval iv) iv -- co
-            TokDummy             -> return ()
-            TokEOF               -> return ()
-    
-    getSourceByInterval :: Interval -> String
-    getSourceByInterval iv = take len $ drop (st - 1) input
-        where
-            st  = (fromIntegral . posPos . iStart) iv
-            end = (fromIntegral . posPos . iEnd) iv
-            len = end - st
-    
-    getSourceByRange :: Range -> String
-    getSourceByRange (Range ivs) = foldl (++) [] $ map getSourceByInterval ivs
-
-type LabeledSource = Kate.Token -- ([String], String)
-
-data SourceLineState = SLS
-    { slsLines :: [SourceLine]
-    , slsCurrentLine :: !Int
-    , slsCurrentChar :: !Int
-    } deriving (Show)
-
-newtype SourceLineGen a = SLG (StateT SourceLineState IO a)
-    deriving (Monad, MonadState SourceLineState, MonadIO)
-
-newLine :: SourceLineGen ()
-newLine = modify (\s -> s
-    { slsLines = (slsLines s) ++ [[]]
-    , slsCurrentLine = (slsCurrentLine s) + 1
-    , slsCurrentChar = 1
-    })
-
-extendCurrentLine :: LabeledSource -> SourceLineGen ()
-extendCurrentLine ls@(attrs, source) = modify (\s -> s { slsLines = modLines s, slsCurrentChar = modChars s })
-    where
-        modChars s = (slsCurrentChar s) + (length source)
-        modLines s = (start s) ++ [ modLine s ] ++ (end s)
-        modLine  s = ((slsLines s) !! ((slsCurrentLine s) - 1)) ++ [ ls ]
-        start    s = fst $ parts s
-        end      s = drop 1 $ snd $ parts s
-        parts    s = splitAt ((slsCurrentLine s) - 1) (slsLines s)
-
-addAt :: LabeledSource -> Int -> Int -> SourceLineGen ()
-addAt ls line char = do
-    currentLine <- gets slsCurrentLine
-    let lineDiff = line - currentLine - 1
-    mapM_ (\x -> newLine) [0..lineDiff]
-    currentChar <- gets slsCurrentChar
-    let charDiff = char - currentChar
-    if charDiff > 0 then extendCurrentLine $ spaceLS charDiff else return ()
-    extendCurrentLine ls
-    where
-        spaceLS n = (OtherTok, replicate n ' ')
-
-addAtPosition :: LabeledSource -> Position -> SourceLineGen ()
-addAtPosition ls p = addAt ls (fromIntegral $ posLine p) (fromIntegral $ posCol p)
-
-addByInterval :: LabeledSource -> Interval -> SourceLineGen ()
-addByInterval ls i = addAtPosition ls (iStart i)
-
-addByRange :: LabeledSource -> Range -> SourceLineGen ()
-addByRange ls (Range is) = mapM_ (addByInterval ls) is
-
-runSourceLineGen :: SourceLineGen a -> [SourceLine]
-runSourceLineGen (SLG body) = slsLines $ unsafePerformIO $ execStateT body (SLS
-    { slsLines = [[]]
-    , slsCurrentLine = 1
-    , slsCurrentChar = 1
-    })
diff --git a/Args.hs b/Args.hs
--- a/Args.hs
+++ b/Args.hs
@@ -29,7 +29,7 @@
         , port          :: Int
         , lang          :: String
         , static        :: Bool
-        , verbose       :: Bool
+        , verbose       :: Int
         , verboseinterpreter :: Bool
         , recompilecmd  :: String
         , magicname     :: String
@@ -39,7 +39,7 @@
 myargs :: Args
 myargs = Args
         { sourcedir     = "."     &= typDir         &= help "Directory of lhs files to serve. Default is '.'"
-        , includedir    = []      &= typDir         &= help "Additional include directory (eg. path of Agda Standard Library). You can specify more than one. Empty by default."
+        , includedir    = []      &= typDir         &= help "Additional include directory. You can specify more than one. Empty by default."
         , gendir        = "html"  &= typDir         &= help "Directory to put generated content to serve. Default is 'html'"
         , exercisedir   = "exercise" &= typDir      &= help "Directory to put generated exercises to serve. Default is 'exercise'"
         , templatedir   = ""      &= typDir         &= help "Directory of html template files for pandoc. Default points to the distribution's directory."
@@ -54,7 +54,7 @@
         , lang          = "en"    &= typ "LANGUAGE" &= help "Default language. It is 'en' by default."
         , port          = 8000    &= typ "PORT"     &= help "Port to listen"
         , static        = False                     &= help "Do not regenerate pages."
-        , verbose       = False                     &= help "Verbose activehs output"
+        , verbose       = 2                         &= help "Verbose activehs output"
         , verboseinterpreter = False                &= help "Verbose interpreter output in the browser"
         , recompilecmd  = "ghc -O" &= typ "COMMAND" &= help "Command to run before page generation. Default is 'ghc -O'."
         , magicname    = "a9xYf"  &= typ "VARNAME"  &= help "Magic variable name."
diff --git a/Cache.hs b/Cache.hs
--- a/Cache.hs
+++ b/Cache.hs
@@ -6,7 +6,7 @@
     , clearCache
     ) where
 
-import Data.Digest.Pure.MD5 (MD5Digest)
+import Hash
 
 import Control.Concurrent.MVar (MVar, newEmptyMVar, readMVar, putMVar)
 import Data.Array.IO (IOArray, newArray, readArray, writeArray, getBounds)
@@ -22,7 +22,7 @@
 
 data CacheEntry a
     = CacheEntry 
-        { question :: MD5Digest
+        { question :: Hash
         , answer   :: MVar a
         }
 
@@ -39,7 +39,7 @@
     mapM_ (\i -> writeArray (array c) i []) [a..b]
 
 
-lookupCache :: Cache a -> MD5Digest -> IO (Either a (a -> IO ()))
+lookupCache :: Cache a -> Hash -> IO (Either a (a -> IO ()))
 lookupCache ch e = modifyCacheLine (array ch) (getIndex e) $ \vv ->
     case lookupIA (cacheLineSize ch) (\x -> e == question x) vv of
         (Just x_, c) -> do
@@ -63,7 +63,7 @@
         writeArray ch i x'
         return r
 
-    getIndex :: MD5Digest -> Int
+    getIndex :: Hash -> Int
     getIndex e = 16 * digitToInt a + digitToInt b where (a:b:_) = show e
 
 
diff --git a/CheckAgdaCode.hs b/CheckAgdaCode.hs
deleted file mode 100644
--- a/CheckAgdaCode.hs
+++ /dev/null
@@ -1,175 +0,0 @@
-module CheckAgdaCode
-    ( typeCheckAgdaCode
-    ) where
-
---import Smart
---import ActiveHs.Base (WrapData2 (WrapData2), TestCase (TestCase))
-import Lang
-import qualified Result as AHR
---import Qualify (qualify)
-
-import Data.Digest.Pure.MD5
---import Language.Haskell.Interpreter hiding (eval)
-
-import Agda.Interaction.GhciTop
-
---import Data.Char (isLower)
---import Data.List (intercalate)
---import Control.Concurrent.MVar
-
-
-import System.Directory
---import qualified System.IO as IO
---import System.IO.Unsafe
---import Data.Char
---import Data.Maybe
---import Data.IORef
---import Data.Function
-import Control.Applicative
---import qualified Control.Exception as E
-
---import Agda.Utils.Fresh
---import Agda.Utils.Monad
---import Agda.Utils.Pretty as P
---import Agda.Utils.String
-import Agda.Utils.FileName
---import qualified Agda.Utils.Trie as Trie
---import Agda.Utils.Tuple
---import qualified Agda.Utils.IO.UTF8 as UTF8
-
-import Control.Monad.Error
---import Control.Monad.Reader
-import Control.Monad.State hiding (State)
---import Control.Exception
---import Data.List as List
---import qualified Data.Map as Map
---import System.Exit
---import qualified System.Mem as System
---import System.Time
---import Text.PrettyPrint
-
-import Agda.TypeChecker
-import Agda.TypeChecking.Monad as TM
-  hiding (initState, setCommandLineOptions)
-import qualified Agda.TypeChecking.Monad as TM
-import Agda.TypeChecking.MetaVars
-import Agda.TypeChecking.Reduce
-import Agda.TypeChecking.Errors
-
-import Agda.Syntax.Fixity
-import Agda.Syntax.Position
-import Agda.Syntax.Parser
-import qualified Agda.Syntax.Parser.Tokens as T
-import Agda.Syntax.Concrete as SC
-import Agda.Syntax.Common as SCo
-import Agda.Syntax.Concrete.Name as CN
-import Agda.Syntax.Concrete.Pretty ()
-import Agda.Syntax.Abstract as SA
-import Agda.Syntax.Abstract.Pretty
-import Agda.Syntax.Internal as SI
-import Agda.Syntax.Scope.Base
-import Agda.Syntax.Scope.Monad hiding (bindName, withCurrentModule)
-import qualified Agda.Syntax.Info as Info
-import Agda.Syntax.Translation.ConcreteToAbstract
-import Agda.Syntax.Translation.AbstractToConcrete hiding (withScope)
-import Agda.Syntax.Translation.InternalToAbstract
-import Agda.Syntax.Abstract.Name
-
-import Agda.Interaction.EmacsCommand
-import Agda.Interaction.Exceptions
-import Agda.Interaction.FindFile
-import Agda.Interaction.Options
-import Agda.Interaction.MakeCase
-import qualified Agda.Interaction.BasicOps as B
-import Agda.Interaction.Highlighting.Emacs
-import Agda.Interaction.Highlighting.Generate
-import Agda.Interaction.Highlighting.Precise (HighlightingInfo)
-import qualified Agda.Interaction.Imports as Imp
-
-import Agda.Termination.TermCheck
-
-import qualified Agda.Compiler.Epic.Compiler as Epic
-import qualified Agda.Compiler.MAlonzo.Compiler as MAlonzo
-import qualified Agda.Compiler.JS.Compiler as JS
-
-import qualified Agda.Auto.Auto as Auto
-
-import Agda.Utils.Impossible
-
-
-
-
-
-typeCheckAgdaCode
-    :: [FilePath] -> MD5Digest -> Language -> {-TaskChan -> -}FilePath -> String 
-    -> IO [AHR.Result]
-typeCheckAgdaCode sourcedirs m5 lang {-ch-} fn ft
-    = do
-        s <- ioTCM' fn False (cmd_load fn $ "." : sourcedirs)
-        return $ case s of
-                    Nothing -> [AHR.Message "Right!" Nothing]
-                    Just err -> [AHR.Error True err]
-
-ioTCM' :: FilePath
-         -- ^ The current file. If this file does not match
-         -- 'theCurrentFile', and the 'Interaction' is not
-         -- \"independent\", then an error is raised.
-      -> Bool
-         -- ^ Should syntax highlighting information be produced? In
-         -- that case this function will generate an Emacs command
-         -- which interprets this information.
-      -> Interaction
-      -> IO (Maybe String)
-ioTCM' current highlighting cmd = undefined 
-{-
- infoOnException $ do
-
---  current <- absolute current
-
-  -- Read the state.
-  let (InteractionState { theTCState = st }) = initState
-
-  -- Run the computation.
-  r <- runTCM $ catchError (do
-           put st
-           x  <- withEnv (initEnv
-                            { envEmacs                   = True
-                            , envInteractiveHighlighting = highlighting
-                            }) $ do
-                   case independence cmd of
-                     Dependent             -> ensureFileLoaded current
-                     Independent Nothing   ->
-                       -- Make sure that the include directories have
-                       -- been set.
-                       setCommandLineOptions' =<< commandLineOptions
-                     Independent (Just is) -> do
-                       ex <- liftIO $ doesFileExist $ filePath current
-                       setIncludeDirs is $
-                         if ex then ProjectRoot current else CurrentDir
-                   command $ {-makeSilent-} cmd
-           st <- get
-           return (Right (x, st))
-         ) (\e -> do
-           pers <- stPersistent <$> get
-           s    <- prettyError e
-           return (Left (pers, s, e))
-         )
-
-  -- If an error was encountered, display an error message and exit
-  -- with an error code; otherwise, inform Emacs about the buffer's
-  -- goals (if current matches the new current file).
-  let errStatus = Status { sChecked               = False
-                         , sShowImplicitArguments =
-                             optShowImplicit $ stPragmaOptions st
-                         }
-  case r of
-    Right (Left (_, s, e)) -> displayErrorAndExit errStatus (getRange e) s
-    Left e                 -> displayErrorAndExit errStatus (getRange e) $
-                                tcErrString e
-    Right (Right _)        -> return Nothing
- where
-  displayErrorAndExit es range err = return $ Just err
--}
-
-
-
diff --git a/Converter.hs b/Converter.hs
--- a/Converter.hs
+++ b/Converter.hs
@@ -6,18 +6,16 @@
 
 import Parse
 
-import Smart (TaskChan, restart, mkId, interp)
+import Smart (TaskChan, restart, interp)
 import Result (hasError)
 import Html
 import Lang
 import Args
+import Hash
 
 import qualified Language.Haskell.Exts.Pretty as HPty
 import qualified Language.Haskell.Exts.Syntax as HSyn
 
-import qualified Agda.Syntax.Concrete as ASyn
-import qualified Agda.Utils.Pretty as AUtil
-
 import Text.XHtml.Strict hiding (lang)
 import Text.Pandoc
 
@@ -26,10 +24,11 @@
 import System.FilePath
 import System.Exit
 import System.Directory (getTemporaryDirectory, getModificationTime, doesFileExist, getTemporaryDirectory, createDirectoryIfMissing)
-import System.Time (diffClockTimes, noTimeDiff) 
+--import Data.Time (diffUTCTime) 
 
 import Control.Monad
 import Data.List
+import Data.Char
 
 ----------------------------------
 
@@ -37,7 +36,7 @@
 convert ghci args@(Args {magicname, sourcedir, gendir, recompilecmd, verbose}) what = do
     whenOutOfDate () output input $ do
         whenOutOfDate () object input $ do
-            when verbose $ putStrLn $ object ++ " is out of date, regenerating"
+            when (verbose > 0) $ putStrLn $ object ++ " is out of date, regenerating"
 --            x <- system $ recompilecmd ++ " " ++ input
             let (ghc:args) = words recompilecmd -- !!!
             (x, out, err) <- readProcessWithExitCode ghc (args ++ [input]) ""
@@ -46,16 +45,10 @@
                     restart ghci
                     return ()
                 else fail $ unlines [unwords [recompilecmd, input], show x, out, err]
-        when verbose $ putStrLn $ output ++ " is out of date, regenerating"
-        mainParse HaskellMode input  >>= extract HaskellMode verbose ghci args what
-    whenOutOfDate () output input2 $ do
-    -- watch object code (*.lagdai?) like in haskell mode?
-        when verbose $ putStrLn $ output ++ " is out of date, regenerating"
-        mainParse AgdaMode input2 >>= extract AgdaMode verbose ghci args what
---        return True
+        when (verbose > 0) $ putStrLn $ output ++ " is out of date, regenerating"
+        mainParse HaskellMode input  >>= extract HaskellMode (verbose > 0) ghci args what
  where
     input  = sourcedir  </> what <.> "lhs"
-    input2 = sourcedir  </> what <.> "lagda"
     output = gendir     </> what <.> "xml"
     object = sourcedir  </> what <.> "o"
 
@@ -68,7 +61,7 @@
     ht <- readFile' $ templatedir </> lang' ++ ".template"
 
     writeFile' (gendir </> what <.> "xml") $ flip writeHtmlString (Pandoc meta $ concat ss')
-      $ defaultWriterOptions
+      $ def
         { writerStandalone      = True
         , writerTableOfContents = True
         , writerSectionDivs     = True
@@ -78,7 +71,6 @@
  where
     ext = case mode of
         HaskellMode -> "hs"
-        AgdaMode    -> "agda"
     
     lang' = case span (/= '_') . reverse $ what of
         (l, "")                -> lang
@@ -106,8 +98,7 @@
             HPty.prettyPrint $ 
               HSyn.Module loc (HSyn.ModuleName "Main") directives Nothing Nothing
                 ([mkImport modname funnames, mkImport_ ('X':magicname) modname] ++ imps) []
-        AgdaModule (directives, ASyn.Module loc modname _ _ : _) -> "open import " ++ show modname ++ " hiding ( " ++ intercalate "; " funnames ++ " )" 
-        _ -> error "error in Converter.extract"
+--        _ -> error "error in Converter.extract"
 
     mkCodeBlock l =
         [ CodeBlock ("", ["haskell"], []) $ intercalate "\n" l | not $ null l ]
@@ -121,7 +112,7 @@
         = return $ mkCodeBlock $ visihidden
 
     processBlock _ (Exercise _ visi hidden funnames is) = do
-        let i = show $ mkId $ unlines funnames
+        let i = show $ mkHash $ unlines funnames
             j = "_j" ++ i
             fn = what ++ "_" ++ i <.> ext
             (static_, inForm, rows) = if null hidden
@@ -138,7 +129,7 @@
     processBlock ii (OneLineExercise 'H' erroneous exp) 
         = return []
     processBlock ii (OneLineExercise p erroneous exp) = do
-        let m5 = mkId $ show ii ++ exp
+        let m5 = mkHash $ show ii ++ exp
             i = show m5
             fn = what ++ (if p == 'R' then "_" ++ i else "") <.> ext
             act = getOne "eval" fn i i
@@ -160,7 +151,7 @@
     processBlock _ (Text (CodeBlock ("",[t],[]) l)) 
         | t `elem` ["dot","neato","twopi","circo","fdp","dfdp","latex"] = do
             tmpdir <- getTemporaryDirectory
-            let i = show $ mkId $ t ++ l
+            let i = show $ mkHash $ t ++ l
                 fn = what ++ i
                 imgname = takeFileName fn <.> "png"
                 outfile = gendir </> fn <.> "png"
@@ -209,7 +200,7 @@
     isLim (Text HorizontalRule) = True
     isLim _ = False
 
-    isHeader (Text (Header _ _)) = True
+    isHeader (Text (Header {})) = True
     isHeader _ = False
 
 ------------------------------------
@@ -243,10 +234,6 @@
     =  "{-# LINE 1 \"testenv\" #-}\n"
     ++ prelude
     ++ "\n{-# LINE 1 \"input\" #-}\n"
-showEnv AgdaMode prelude
-    =  "{- LINE 1 \"testenv\" -}\n"
-    ++ prelude
-    ++ "\n{- LINE 1 \"input\" -}\n"
 
 mkImport :: String -> [Name] -> HSyn.ImportDecl
 mkImport m d 
@@ -257,9 +244,14 @@
         , HSyn.importSrc = False
         , HSyn.importPkg = Nothing
         , HSyn.importAs = Nothing
-        , HSyn.importSpecs = Just (True, map (HSyn.IVar . HSyn.Ident) d)
+        , HSyn.importSpecs = Just (True, map (HSyn.IVar . mkName) d)
         }
 
+mkName :: String -> HSyn.Name
+mkName n@(c:_)
+    | isSymbol c = HSyn.Symbol n
+mkName n = HSyn.Ident n
+
 mkImport_ :: String -> String -> HSyn.ImportDecl
 mkImport_ magic m 
     = (mkImport m []) { HSyn.importQualified = True, HSyn.importAs = Just $ HSyn.ModuleName magic }
@@ -272,7 +264,7 @@
     b <- modTime src
     case (a, b) of
         (Nothing, Just _) -> m
-        (Just t1, Just t2) | diffClockTimes t2 t1 > noTimeDiff -> m
+        (Just t1, Just t2) | t1 < t2 -> m
         _   -> return def
  where
     modTime f = do
diff --git a/Hash.hs b/Hash.hs
new file mode 100644
--- /dev/null
+++ b/Hash.hs
@@ -0,0 +1,14 @@
+module Hash
+    ( Hash
+    , mkHash
+    ) where
+
+import Data.Digest.Pure.MD5 hiding (Hash)
+import Data.ByteString.Lazy.UTF8 (fromString)
+
+type Hash = MD5Digest
+
+mkHash :: String -> Hash
+mkHash = md5 . fromString
+
+
diff --git a/Logger.hs b/Logger.hs
new file mode 100644
--- /dev/null
+++ b/Logger.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE ViewPatterns, PatternGuards, OverloadedStrings #-}
+module Logger
+    ( Logger
+    , newLogger
+    , logMsg
+    , logStrMsg
+    ) where
+
+import qualified System.FastLogger as SF
+
+import Control.Applicative
+import Control.Monad
+
+import qualified Data.ByteString as B
+import qualified Data.ByteString.UTF8 as B
+
+-------
+
+
+data Logger = Logger
+    { logger :: SF.Logger
+    , level  :: Int
+        -- 0: very important message, usually an error report, wrapped in '#####'
+        -- 1: important message, wrapped in '####'
+        -- 2: normal message
+        -- 3, 4, ...: debug messages (not shown by default)
+    }
+
+newLogger :: Int -> FilePath -> IO Logger
+newLogger l path
+    = Logger <$> SF.newLogger path <*> pure l
+
+logStrMsg :: Int -> Logger -> String -> IO ()
+logStrMsg l lg
+    = logMsg l lg . B.fromString
+
+logMsg :: Int -> Logger -> B.ByteString -> IO ()
+logMsg l lg msg = do
+    msg' <- SF.timestampedLogEntry $ highlight l msg
+    when (l <= level lg) $ SF.logMsg (logger lg) msg'
+  where
+    highlight 0 = wrap "#####"
+    highlight 1 = wrap "####"
+    highlight _ = id
+
+    wrap n x = B.concat [n, "    ", x, "    ", n]
+
diff --git a/Main.hs b/Main.hs
--- a/Main.hs
+++ b/Main.hs
@@ -9,34 +9,29 @@
 import Args
 import Special
 import Lang
+import Logger
 import Result
 import Html
+import Hash
+import Snap
 
 import Snap.Core
 import Snap.Http.Server (httpServe)
 import Snap.Http.Server.Config
 import Snap.Util.FileServe (getSafePath, serveDirectoryWith, simpleDirectoryConfig)
 
-import Data.Digest.Pure.MD5 (md5)
-import System.FastLogger
-
 import qualified Data.Text as T
 import qualified Data.Text.IO as T
-import Data.Text.Encoding (decodeUtf8With)
-import Data.Text.Encoding.Error (lenientDecode)
-import Data.ByteString (ByteString)
-import Data.ByteString.UTF8 (fromString)
-import qualified Data.ByteString.Lazy.UTF8 as Lazy
 
 import System.FilePath ((</>), takeExtension, dropExtension)
 import System.Directory (doesFileExist)
-import Language.Haskell.Interpreter (liftIO)
 import Control.Concurrent (threadDelay)
 import Control.Monad (when)
 import Control.Applicative ((<|>))
-import Data.Time (getCurrentTime, diffUTCTime)
+import System.Locale (defaultTimeLocale)
+import Data.Time (getCurrentTime, formatTime, diffUTCTime)
 import Data.Maybe (listToMaybe)
-import Prelude hiding (catch)
+--import Prelude hiding (catch)
 
 ---------------------------------------------------------------
 
@@ -44,9 +39,14 @@
 main = getArgs >>= mainWithArgs
 
 mainWithArgs :: Args -> IO ()
-mainWithArgs args@(Args {port, static, logdir, hoogledb, fileservedir, gendir, mainpage, restartpath, sourcedir, includedir}) = do 
+mainWithArgs args@(Args {verbose, port, static, logdir, hoogledb, fileservedir, gendir, mainpage, restartpath, sourcedir, includedir}) = do 
 
-    ch <- startGHCiServer [sourcedir] (logdir </> "interpreter") hoogledb
+    ti <- getCurrentTime
+    log <- newLogger verbose $ 
+        logdir </> "interpreter_" ++ formatTime defaultTimeLocale "%Y-%m-%d-%H-%M-%S" ti ++ ".log"
+             -- "%Y-%m-%d-%H:%M:%S" is not ok, colons are not supported in filenames under windows
+
+    ch <- startGHCiServer [sourcedir] log hoogledb
     cache <- newCache 10
 
     httpServe
@@ -60,8 +60,8 @@
         (   method GET
                 (   serveDirectoryWith simpleDirectoryConfig fileservedir
                 <|> serveHtml ch
-                <|> ifTop (redirect $ fromString mainpage)
-                <|> path (fromString restartpath) (liftIO $ restart ch >> clearCache cache)
+                <|> ifTop (redirectString mainpage)
+                <|> pathString restartpath (liftIO $ restart ch >> clearCache cache)
                 )
         <|> method POST (exerciseServer (sourcedir:includedir) (cache, ch) args)
         <|> notFound
@@ -79,20 +79,8 @@
         getResponse >>= finishWith . setResponseCode 404
 
 
-
-
-
-
 ---------------------------------------------------------------
 
-logNormalMsg :: TaskChan -> String -> IO ()
-logNormalMsg ch x = do
-    v <- timestampedLogEntry $ fromString x
-    logMsg (logger ch) v 
-
-getParam' :: ByteString -> Snap (Maybe T.Text)
-getParam' = fmap (fmap $ decodeUtf8With lenientDecode) . getParam
-
 type TaskChan' = (Cache (Int, T.Text), TaskChan)
 
 exerciseServer :: [FilePath] -> TaskChan' -> Args -> Snap ()
@@ -102,18 +90,18 @@
         writeText "<html xmlns=\"http://www.w3.org/1999/xhtml\"><body>Too long request.</body></html>"
         getResponse >>= finishWith . setResponseCode 400
 
-    let md5Id = md5 $ Lazy.fromString params   -- could be more efficient
-    liftIO $ logNormalMsg ch $ " eval " ++ show md5Id ++ " " ++ params
+    let md5Id = mkHash params   -- could be more efficient
+    liftIO $ logStrMsg 2 (logger ch) $ " eval " ++ show md5Id ++ " " ++ params
     j <- liftIO $ lookupCache cache md5Id
     (>>= writeText) $ case j of
       Left (delay, res) -> liftIO $ do
-        logNormalMsg ch $ "   ch " ++ show md5Id
+        logStrMsg 2 (logger ch) $ "   ch " ++ show md5Id
         threadDelay delay
         return res
       Right cacheAction -> do
         time <- liftIO $ getCurrentTime
         res <- fmap renderResults $ do
-            Just [ss, fn_, x, y, T.unpack -> lang']  <- fmap sequence $ mapM getParam' ["c","f","x","y","lang"]
+            Just [ss, fn_, x, y, T.unpack -> lang']  <- fmap sequence $ mapM getTextParam ["c","f","x","y","lang"]
 
             let fn = exercisedir </> T.unpack fn_
                 ext = reverse $ takeWhile (/='.') $ reverse fn
@@ -126,7 +114,7 @@
         liftIO $ do
             time' <- getCurrentTime
             let delay = round $ 1000000 * (realToFrac $ diffUTCTime time' time :: Double) :: Int
-            logNormalMsg ch $ "  end " ++ show md5Id ++ " " ++ show delay ++ " ms  " ++ T.unpack res
+            logStrMsg 2 (logger ch) $ "  end " ++ show md5Id ++ " " ++ show delay ++ " ms  " ++ T.unpack res
             cacheAction (delay, res)
             return res
 
diff --git a/Parse.hs b/Parse.hs
--- a/Parse.hs
+++ b/Parse.hs
@@ -15,29 +15,24 @@
 
 import Text.Pandoc
 
-import AgdaHighlight
-
 import qualified Language.Haskell.Exts.Parser as HPar
 import qualified Language.Haskell.Exts.Syntax as HSyn
 
-{- Agda support (unfinished) -}
-import qualified Agda.Syntax.Parser as APar
-import qualified Agda.Syntax.Concrete as ASyn
-
 import Data.List.Split (splitOn)
 import Data.List (tails, partition, groupBy)
 import Data.Function (on)
 import Data.Char (isAlpha, isSpace, toUpper, isUpper)
 import Control.Monad (zipWithM)
+import qualified Data.Set as Set
 
 --------------------------------- data structures
 
-data ParseMode = HaskellMode | AgdaMode
+data ParseMode = HaskellMode -- | AgdaMode
                  deriving (Show, Enum, Eq)
 
 data Module
     = HaskellModule HSyn.Module
-    | AgdaModule ASyn.Module
+--    | AgdaModule ASyn.Module
     deriving (Show)
 
 data Doc
@@ -85,7 +80,6 @@
             fmap (Doc meta header) $ collectTests mode $ map ({-highlight . -}interpreter . Text) blocks
     where
         parseModule :: ParseMode -> String -> IO Module
-        parseModule AgdaMode    m = fmap AgdaModule (APar.parse APar.moduleParser m)
         parseModule HaskellMode m = case HPar.parseModuleWithMode HPar.defaultParseMode m of
             (HPar.ParseOk m) -> return $ HaskellModule m
             parseError       -> fail $ "parseHeader: " ++ show parseError
@@ -98,10 +92,10 @@
         preprocess l | take 3 (dropWhile (==' ') $ reverse l) == "-- " = []
                      | otherwise = [l]
         
-        pState = defaultParserState 
-            { stateSmart = True
-            , stateStandalone = True
-            , stateLiterateHaskell = True 
+        pState = def
+            { readerSmart = True
+            , readerStandalone = True
+            , readerExtensions = Set.insert Ext_literate_haskell $ readerExtensions def
             }
         
         interpreter :: BBlock -> BBlock
@@ -109,11 +103,6 @@
             = OneLineExercise (toUpper x) (isUpper x) e
         interpreter a = a
         
-        highlight :: BBlock -> BBlock
-        highlight (Text (CodeBlock ("",["sourceCode","literate","haskell"],[]) code)) | mode == AgdaMode
-            = (Text (RawBlock "html" $ highlightAgdaAsXHtml code))
-        highlight a = a
-
 ------------------------------
 
 collectTests :: ParseMode -> [BBlock] -> IO [BBlock]
@@ -135,38 +124,7 @@
     f x _ = return x
 
 processLines :: ParseMode -> Bool -> String -> IO ([String], [String], [Name])
-processLines AgdaMode    = processAgdaLines
 processLines HaskellMode = processHaskellLines
-
-{- Agda support (unfinished) -}
-processAgdaLines :: Bool -> String -> IO ([String], [String], [Name])
-processAgdaLines isExercise l_ = do
---    return ([], [], [])
-
-    let
-        l = parts l_
-
-    x <- fmap (zip l) $ mapM (APar.parse APar.moduleParser . ("module X where\n"++) . unlines) l
-    let
-        names = map toName $ concatMap (getFName . snd . snd) x
-
---        getFName [Agda.Module _ _ [Agda.TypedBindings _ (Agda.Arg _ _ [Agda.TBind _ a _])] declarations] 
---                  = map Agda.boundName a
-        getFName [ASyn.Module _ _ _ [ASyn.TypeSig _ n _]]
-                  = [n]
-        getFName _ = []
-
---        isVisible [Agda.Module _ _ [Agda.TypedBindings _ (Agda.Arg _ _ [Agda.TBind _ a _])] declarations] 
---                    = True
-        isVisible [ASyn.Module _ _ _ [ASyn.TypeSig _ n _]] = True
-        isVisible _ = not isExercise
-
-        (visible, hidden) = partition (isVisible . snd . snd) x
-
-        toName n = {- HSyn.Ident $-} show n
-
-    return (concatMap fst visible, concatMap fst hidden, names)
-
 
 processHaskellLines :: Bool -> String -> IO ([String], [String], [Name])
 processHaskellLines isExercise l_ = return (concatMap fst visible, concatMap fst hidden, names)
diff --git a/QuickCheck.hs b/QuickCheck.hs
--- a/QuickCheck.hs
+++ b/QuickCheck.hs
@@ -4,35 +4,51 @@
 import ActiveHs.Base (WrapData2 (WrapData2), TestCase (TestCase))
 import Lang
 import Result
+import Logger
 import Qualify (qualify)
+import Hash
 
-import Data.Digest.Pure.MD5
-import Language.Haskell.Interpreter hiding (eval)
 import Test.QuickCheck hiding (Result)
 import qualified Test.QuickCheck.Property as QC
 
 import Data.Char (isLower)
 import Data.List (intercalate)
+import Control.Monad (join)
 import Control.Concurrent.MVar
 
 ---------------------------------------
 
 quickCheck
-    :: String -> MD5Digest -> Language -> TaskChan -> FilePath -> String -> [String] -> [([String],String)] 
+    :: String
+    -> Hash
+    -> Language
+    -> TaskChan
+    -> FilePath
+    -> String
+    -> [String]
+    -> [([String],String)]      -- test cases
     -> IO [Result]
-quickCheck qualifier m5 lang ch fn ft funnames is
-    = case allRight $ map (qualify qualifier funnames . snd) is of
-        Left err -> return [Error True err]
-        Right s_ -> interp False m5 lang ch fn "" $ \a ->
-            do  m <- interpret (mkTestCases [(v,s,s') | ((v,s),s')<- zip is s_]) (as :: [TestCase])
-                return $ qcs lang m
+quickCheck qualifier m5 lang ch fn ft funnames testcases = do
+    logStrMsg 3 (logger ch) $ "test cases: " ++ show testcases
+    logStrMsg 3 (logger ch) $ "names to be qualified: " ++ show funnames
 
-  where
-    allRight :: [Either a b] -> Either a [b]
-    allRight x = case [s | Left s<-x] of
-        (y:_) -> Left y
-        []    -> Right [s | Right s<-x]
+    case allRight $ map (qualify qualifier funnames . snd) testcases of
+        Left err -> do
+            logStrMsg 3 (logger ch) $ "Error in qualification: " ++ err
+            return [Error True err]
+        Right s_ -> do
+            logStrMsg 3 (logger ch) $ "Qualified expressions: " ++ show s_
 
+            let ts = mkTestCases [(v,s,s') | ((v,s),s')<- zip testcases s_]
+            logStrMsg 3 (logger ch) $ "Test cases: " ++ ts
+            
+            interp False m5 lang ch fn "" $ \a ->
+                do  liftIO $ logStrMsg 3 (logger ch) "Before interpretation"
+                    m <- interpret ts (as :: [TestCase])
+                    liftIO $ logStrMsg 3 (logger ch) "After interpretation"
+                    return $ qcs lang (logger ch) m
+
+  where
     mkTestCases ss 
         = "[" ++ intercalate ", " (map mkTestCase ss) ++ "]"
 
@@ -41,7 +57,6 @@
         ++ unwords ["(" ++ v ++ ")" | v<-vars] 
         ++ " -> qcinner (" ++ showTr vars s ++ ", " ++ parens s ++ ", " ++ parens s2 ++ "))"
 
-
     showTr vars s = "unwords [" ++ intercalate ", " (map g $ words s) ++ "]"  -- !!!
      where
 
@@ -52,31 +67,39 @@
         g x | x `elem` vs = {- "\"(\" ++ -} " show " ++ x -- ++ " ++ \")\""
         g x = show x
 
-qcs :: Language -> [TestCase] -> IO [Result]
-qcs lang [] = return [Message (translate lang "All test cases are completed.") Nothing]
-qcs lang (t:ts) = do
-    s' <- qc lang t
-    case s' of
-        Just rep -> rep
-        Nothing  -> qcs lang ts
+qcs :: Language -> Logger -> [TestCase] -> IO [Result]
+qcs lang log = join . foldM (return [Message (translate lang "All test cases are completed.") Nothing]) (qc lang log)
 
 -- test = qc $ TestCase $ \f (QCNat x) (QCInt y) -> f (show x ++ " + " ++ show y, min 10 (x + y), x + y)
 -- test' = qc $ TestCase $ \f (QCInt x) -> f ("sqr " ++ show x, min 10 (x*x), x*x)
 
-qc :: Language -> TestCase -> IO (Maybe (IO [Result]))
-qc lang (TestCase p) = do
+qc :: Language -> Logger -> TestCase -> IO (Maybe (IO [Result]))
+qc lang log (TestCase p) = do
     v <- newMVar Nothing
-    _ <- quickCheckWithResult (stdArgs { chatty = False }) $ {- QC.noShrinking $ -} p $ ff v
+    let ff (s, x, y)
+            = QC.whenFail (modifyMVar_ v $ const $ return $ Just $ fmap (ModifyCommandLine s :) res)
+            $ QC.morallyDubiousIOProperty
+            $ fmap (\s -> if hasError s then QC.failed else QC.succeeded) res
+          where
+            res = do
+                logStrMsg 4 log $ "compare: " ++ s
+                compareClearGen lang "noId" $ WrapData2 x y
+    _ <- quickCheckWithResult (stdArgs { chatty = False }) $ {- QC.noShrinking $ -} p ff
     takeMVar v
- where
-    ff v (s, x, y)
-        = QC.whenFail (modifyMVar_ v $ const $ return $ Just $ fmap (ModifyCommandLine s :) res)
-        $ QC.morallyDubiousIOProperty
-        $ fmap f res
-      where
-        res = compareClearGen lang "noId" $ WrapData2 x y
 
-    f s | hasError s = QC.failed
-    f s = QC.succeeded
+------------------------------------
+
+allRight :: [Either a b] -> Either a [b]
+allRight x = case [s | Left s<-x] of
+    (y:_) -> Left y
+    []    -> Right [s | Right s<-x]
+
+foldM :: Monad m => r -> (a -> m (Maybe r)) -> [a] -> m r
+foldM end _ [] = return end
+foldM end f (t:ts) = do
+    x <- f t
+    case x of
+        Just r -> return r
+        Nothing  -> foldM end f ts
 
 
diff --git a/Result.hs b/Result.hs
--- a/Result.hs
+++ b/Result.hs
@@ -51,8 +51,10 @@
 errors _ = False
 
 filterResults :: [Result] -> [Result]
-filterResults rs = case filter (not . weakError) rs of
-    [] -> take 1 rs
+filterResults rs = case filter (not . weakOrHardError) rs of
+    [] -> case [e | e@(Error True _) <- rs] of
+            [] -> take 1 rs
+            rs -> take 1 rs
     rs -> case filter (not . searchResult) rs of
         [] -> rs
         rs -> {- nubBy f -} rs
@@ -63,14 +65,14 @@
 -}
 
 hasError :: [Result] -> Bool
-hasError rs = case filter (not . weakError) rs of
+hasError rs = case filter (not . weakOrHardError) rs of
     [] -> True
     rs -> any errors rs
 
-weakError :: Result -> Bool
-weakError (Error _ _) = True
-weakError (ExprType b _ _ _) = b
-weakError _ = False
+weakOrHardError :: Result -> Bool
+weakOrHardError (Error _ _) = True
+weakOrHardError (ExprType b _ _ _) = b
+weakOrHardError _ = False
 
 searchResult :: Result -> Bool
 searchResult (SearchResults _ _) = True
diff --git a/Simple.hs b/Simple.hs
--- a/Simple.hs
+++ b/Simple.hs
@@ -4,12 +4,18 @@
     ( Task (..), TaskChan
     , startGHCiServer
     , restartGHCiServer
-    , interpret
+    , sendToServer
     , catchError_fixed
+
+    , Interpreter, typeOf, kindOf
+    , InterpreterError (..), errMsg, interpret
+    , as, liftIO, parens
     ) where
 
-import Language.Haskell.Interpreter hiding (interpret)
+import Logger
 
+import Language.Haskell.Interpreter
+
 import Control.Concurrent (forkIO)
 import Control.Concurrent.MVar (MVar, newEmptyMVar, takeMVar, putMVar)
 import Control.Concurrent.Chan (Chan, newChan, readChan, writeChan)
@@ -17,7 +23,7 @@
 import Control.Monad (when, forever)
 import Control.Monad.Error (MonadError, catchError)
 import Data.List (isPrefixOf)
-import Prelude hiding (catch)
+--import Prelude hiding (catch)
 
 -------------------------
 
@@ -29,17 +35,17 @@
 
 ---------------
 
-startGHCiServer :: [String] -> (String -> IO ()) -> (String -> IO ()) -> IO TaskChan
-startGHCiServer paths{-searchpaths-} logError logMsg = do
+startGHCiServer :: [String] -> Logger -> IO TaskChan
+startGHCiServer paths{-searchpaths-} log = do
     ch <- newChan 
 
     _ <- forkIO $ forever $ do
-        logMsg "start interpreter"
+        logStrMsg 1 log "start interpreter"
         e <- runInterpreter (handleTask ch Nothing)
               `catch` \(e :: SomeException) ->
                 return $ Left $ UnknownError "GHCi server died."
         case e of
-            Left  e  -> logError $ "stop interpreter: " ++ show e
+            Left  e  -> logStrMsg 0 log $ "stop interpreter: " ++ show e
             Right () -> return ()
 
     return $ TC ch
@@ -50,7 +56,7 @@
         task <- lift $ readChan ch
         case task of
             Just task -> handleTask_ ch oldFn task
-            Nothing   -> liftIO $ logError "interpreter stopped intentionally"
+            Nothing   -> liftIO $ logStrMsg 0 log "interpreter stopped intentionally"
 
     handleTask_ ch oldFn (Task fn repVar m) = do
         (cont, res) <- do  
@@ -75,8 +81,8 @@
 restartGHCiServer :: TaskChan -> IO ()
 restartGHCiServer (TC ch) = writeChan ch Nothing
 
-interpret :: TaskChan -> FilePath -> Interpreter a -> IO (Either InterpreterError a)
-interpret (TC ch) fn m = do
+sendToServer :: TaskChan -> FilePath -> Interpreter a -> IO (Either InterpreterError a)
+sendToServer (TC ch) fn m = do
     rep <- newEmptyMVar
     writeChan ch $ Just $ Task fn rep m
     takeMVar rep
diff --git a/Smart.hs b/Smart.hs
--- a/Smart.hs
+++ b/Smart.hs
@@ -1,11 +1,23 @@
 {-# LANGUAGE ViewPatterns, PatternGuards, OverloadedStrings #-}
-module Smart where
+module Smart
+    ( module Simple
+    , startGHCiServer
+    , restart
+    , TaskChan (..)
+    , interp
+    , compareClearGen
+    , compareMistGen
+    , wrap2
+    ) where
 
 import HoogleCustom
 import Specialize
 import Lang
 import Result
+import Logger
+import Simple hiding (TaskChan, startGHCiServer)
 import qualified Simple
+import Hash
 
 import ActiveHs.Base (WrapData2 (..), WrapData(..))
 import Graphics.Diagrams (Diagram)
@@ -18,23 +30,14 @@
 import Data.Data.GenRep.Functions (mistify, numberErrors)
 import Data.Data.GenRep.Doc (toDoc)
 
-import Language.Haskell.Interpreter hiding (eval)
-import Data.Digest.Pure.MD5
 import Hoogle (Database, loadDatabase)
-import System.FastLogger
 
-import System.Locale (defaultTimeLocale)
-import Data.Time (getCurrentTime, formatTime)
-import Data.ByteString.UTF8 (fromString)
-import qualified Data.ByteString as B
-import qualified Data.ByteString.Lazy.UTF8 as Lazy
-
 import Control.Monad (join)
 import Data.Dynamic hiding (typeOf)
 import qualified Data.Data as D
 import Data.List (nub)
 import Data.Char (isAlpha)
-import Prelude hiding (catch)
+--import Prelude hiding (catch)
 
 
 ----------------------------------------------------------------------
@@ -46,22 +49,15 @@
         , chan      :: Simple.TaskChan
         }
 
-startGHCiServer :: [FilePath] -> FilePath -> FilePath -> IO TaskChan
-startGHCiServer searchpaths logfilebase dbname = do
-    ti <- getCurrentTime
- -- log <- newLogger $ logfilebase ++ "_" ++ formatTime defaultTimeLocale "%Y-%m-%d-%H:%M:%S" ti ++ ".log"
- -- colons are not supported in filenames under windows
-    log <- newLogger $ logfilebase ++ "_" ++ formatTime defaultTimeLocale "%Y-%m-%d-%H-%M-%S" ti ++ ".log"
+startGHCiServer :: [FilePath] -> Logger -> FilePath -> IO TaskChan
+startGHCiServer searchpaths log dbname = do
     db <- if (dbname == "") then return Nothing else fmap Just $ loadDatabase dbname
-    ch <- Simple.startGHCiServer
-            searchpaths
-            (logMsgWithImportance 5 log . fromString) 
-            (logMsgWithImportance 4 log . fromString)
+    ch <- Simple.startGHCiServer searchpaths log
     return $ TC
-        { logger    = log
-        , database  = db
-        , chan      = ch
-        }
+            { logger    = log
+            , database  = db
+            , chan      = ch
+            }
 
 restart :: TaskChan -> IO ()
 restart ch = do
@@ -77,23 +73,6 @@
 
 ----------------------------------------------------------------------
 
-logMsgWithImportance :: Int -> Logger -> B.ByteString -> IO ()
-logMsgWithImportance n ch x = do
-    v <- timestampedLogEntry $ B.concat 
-        [nn, "    ", x, "    ", nn]
-    logMsg ch v 
- where
-    nn = fromString $ replicate n '#'
-
-
-
-----------------------------------------------------------------------
-
-mkId :: String -> MD5Digest
-mkId = md5 . Lazy.fromString
-
-------------------
-
 getCommand :: String -> (String, String)
 getCommand (':':'?': (dropSpace -> Just x)) 
     = ("?", x)
@@ -108,7 +87,7 @@
 dropSpace _ = Nothing
 
 
-interp :: Bool -> MD5Digest -> Language -> TaskChan -> FilePath -> String 
+interp :: Bool -> Hash -> Language -> TaskChan -> FilePath -> String 
     -> (String -> Interpreter (IO [Result])) -> IO [Result]
 interp  verboseinterpreter (show -> idi) lang ch fn s@(getCommand -> (c, a)) xy 
     = case c of
@@ -120,7 +99,7 @@
     c | c `elem` ["t","k",""]
        -> join 
         $ fmap (either (return . map (Error True) . showErr lang) id)
-        $ Simple.interpret (chan ch) fn
+        $ sendToServer (chan ch) fn
         $ case c of
             "t" -> catchE True $ do
                 xx <- typeOf a
diff --git a/Snap.hs b/Snap.hs
new file mode 100644
--- /dev/null
+++ b/Snap.hs
@@ -0,0 +1,25 @@
+module Snap where
+
+import Snap.Core
+--import Snap.Http.Server (httpServe)
+--import Snap.Http.Server.Config
+--import Snap.Util.FileServe (getSafePath, serveDirectoryWith, simpleDirectoryConfig)
+
+import Data.Text.Encoding (decodeUtf8With)
+import Data.Text.Encoding.Error (lenientDecode)
+import qualified Data.Text as T
+
+--import Data.ByteString (ByteString)
+import Data.ByteString.UTF8 (fromString)
+
+--------------------
+
+getTextParam :: String -> Snap (Maybe T.Text)
+getTextParam = fmap (fmap $ decodeUtf8With lenientDecode) . getParam . fromString
+
+redirectString :: String -> Snap ()
+redirectString = redirect . fromString
+
+pathString :: String -> Snap () -> Snap ()
+pathString = path . fromString
+
diff --git a/Special.hs b/Special.hs
--- a/Special.hs
+++ b/Special.hs
@@ -6,20 +6,17 @@
 
 import Smart
 import QuickCheck
-import CheckAgdaCode
 import Result
 import Lang
+import Logger
 import Html
 import Qualify (qualify)
+import Hash
 
 import ActiveHs.Base (WrapData2)
 
-import Language.Haskell.Interpreter hiding (eval)
-import Data.Digest.Pure.MD5 (MD5Digest)
-
 import qualified Data.Text as T
 import qualified Data.Text.IO as T
-import Data.ByteString.UTF8 (fromString)
 
 import Control.DeepSeq
 import Control.Concurrent.MVar
@@ -28,7 +25,7 @@
 import System.Directory (getTemporaryDirectory)
 
 import Control.Concurrent (threadDelay, forkIO, killThread)
-import Prelude hiding (catch)
+--import Prelude hiding (catch)
 
 
 ---------------------------------------------------------------
@@ -58,14 +55,14 @@
     -> FilePath
     -> T.Text
     -> Language
-    -> MD5Digest
+    -> Hash
     -> SpecialTask
     -> IO [Result]
 
 exerciseServer' qualifier ch verbose fn sol lang m5 task = do
 
     let error = do
-            logMsgWithImportance 5 (logger ch) $ fromString $ "Server error:" ++ show m5
+            logStrMsg 0 (logger ch) $ "Server error:" ++ show m5
             return [Error True "Server error."]
 
         action =
@@ -100,8 +97,6 @@
                 ss <- quickCheck qualifier m5 lang ch fn' (T.unpack sol) funnames is
                 let ht = head $ [x | ModifyCommandLine x <- ss] ++ [""]
                 return [ShowInterpreter lang 59 (getTwo "eval2" (takeFileName fn) j i j) j 'E' ht ss]
-            "agda" -> do
-                typeCheckAgdaCode sourcedirs m5 lang {-ch-} fn' (T.unpack sol)
 
 tmpSaveHs :: String -> String -> T.Text -> IO FilePath
 tmpSaveHs ext x s = do
@@ -110,7 +105,6 @@
         tmp = tmpdir </> name ++ "." ++ ext
     T.writeFile tmp $ case ext of
         "hs" -> s
-        "agda" -> T.pack ("module " ++ name ++ " where\n\n") `T.append` s
     return tmp
 
 
diff --git a/activehs.cabal b/activehs.cabal
--- a/activehs.cabal
+++ b/activehs.cabal
@@ -1,5 +1,5 @@
 name:                activehs
-version:             0.3.0.1
+version:             0.3.1
 category:            Education, Documentation
 synopsis:            Haskell code presentation tool
 description:
@@ -43,19 +43,19 @@
     Simple,
     Smart,
     Cache,
+    Hash,
     Specialize,
     Qualify,
     Lang,
     Result,
     HoogleCustom,
     Html,
+    Logger,
     QuickCheck,
-    CheckAgdaCode,
-    AgdaHighlight,
+    Snap,
     Special
 
   Build-Depends:
-    Agda >= 2.3.0.1 && < 2.4,
     highlighting-kate >= 0.5 && < 0.6,
     hoogle >= 4.2.11 && < 4.3,
     dia-base >= 0.1 && < 0.2,
@@ -80,12 +80,12 @@
     pureMD5 >= 2.1 && < 2.2,
     deepseq >= 1.1 && < 1.4,
     split >= 0.1 && < 0.3,
-    pandoc >= 1.8 && < 1.10,
+    pandoc >= 1.10 && < 1.11,
     time >= 1.2 && < 1.5,
     old-time >= 1.0 && < 1.2,
     process >= 1.0 && < 1.2,
     hint >= 0.3.3.2 && < 0.4,
-    simple-reflect >= 0.2 && < 0.3,
+    simple-reflect >= 0.2 && < 0.4,
     mtl >= 2.0 && < 2.2,
     old-locale >= 1.0 && < 1.1,
     cmdargs >= 0.7 && < 0.11