diff --git a/AgdaInterface.hs b/AgdaInterface.hs
new file mode 100644
--- /dev/null
+++ b/AgdaInterface.hs
@@ -0,0 +1,47 @@
+module AgdaInterface
+    ( InteractionState
+    , initState
+    , tcmAction_
+
+    , Interaction (..)
+    , Response (..), GiveResult (..)
+    , Range, Range' (..)
+    , InteractionId (..)
+    ) where
+
+import Agda.Interaction.InteractionTop
+import Agda.Interaction.Response
+import Agda.TypeChecking.Monad.Base hiding (initState)
+import qualified Agda.TypeChecking.Monad.Base as Base
+import Agda.Syntax.Position
+
+import Data.IORef
+import Control.Monad.State
+import Control.Concurrent.MVar
+
+-----------------------------
+
+data InteractionState = InteractionState CommandState TCState
+
+initState :: InteractionState
+initState = InteractionState initCommandState Base.initState
+
+tcmAction_
+    :: FilePath
+    -> Interaction
+    -> StateT InteractionState IO [Response]
+tcmAction_ filepath action = StateT $ \(InteractionState cs ts) -> do
+    m <- newMVar []
+
+    let ts_ = ts { stPersistent = (stPersistent ts) { stInteractionOutputCallback = log } }
+        log x = liftIO $ modifyMVar_ m $ return . (x:)
+
+    r <- newIORef ts_
+    cs' <- unTCM (execStateT act cs) r initEnv
+    ts' <- readIORef r
+
+    rs <- fmap reverse $ takeMVar m
+    return (rs, InteractionState cs' ts')
+  where
+    act = runInteraction $ IOTCM filepath Interactive Indirect action
+
diff --git a/Args.hs b/Args.hs
new file mode 100644
--- /dev/null
+++ b/Args.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE DeriveDataTypeable, NamedFieldPuns #-}
+module Args
+    ( getArgs
+    , Args (..)
+    ) where
+
+import Paths_agda_server
+
+import System.Directory (createDirectoryIfMissing)
+import System.Console.CmdArgs.Implicit
+import System.FilePath
+
+import Data.Version
+
+------------------
+
+data Args
+    = Args
+        { sourcedir     :: String
+        , includedir    :: [String]
+        , datadir       :: String
+        , logdir        :: String
+        , port          :: Int
+        }
+        deriving (Show, Data, Typeable)
+
+myargs :: Args
+myargs = Args
+        { sourcedir     = "."     &= typDir         &= help "Directory of agda files to serve. Default is '.'"
+        , includedir    = [""]    &= typDir         &= help "Additional include directory. You can specify more than one. Default is '.'"
+        , datadir       = ""      &= typDir         &= help "Directory of template. Default points to the distribution's directory."
+        , logdir        = "log"   &= typDir         &= help "Directory to put log files in. Default is 'log'."
+        , port          = 8001    &= typ "PORT"     &= help "Port to listen. Default is 8001"
+        }  &= summary ("agda-server " ++ showVersion version ++ ", (C) 2012-2013 Péter Diviánszky")
+           &= program "agda-server"
+
+completeArgs :: Args -> IO Args
+completeArgs args
+    | datadir args == "" = do
+        dir <- getDataDir
+        completeArgs (args {datadir = dir </> "copy"})
+completeArgs args = return args
+
+
+createDirs :: Args -> IO ()
+createDirs (Args {sourcedir, logdir}) 
+    = mapM_ f [sourcedir, logdir]
+ where
+    f "" = return ()
+    f path = createDirectoryIfMissing True path
+
+
+getArgs :: IO Args
+getArgs = do
+    args <- cmdArgs myargs >>= completeArgs
+    createDirs args
+    return args
+
+
+
diff --git a/Html.hs b/Html.hs
new file mode 100644
--- /dev/null
+++ b/Html.hs
@@ -0,0 +1,156 @@
+-- An interface to construct Html data
+--    (later: dedicated data type)
+
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE PatternGuards #-}
+
+module Html
+    ( code'
+    , showR
+    ) where
+
+import Memo
+import JS
+
+import Agda.Interaction.Response
+import Agda.Interaction.Highlighting.Precise
+import qualified Agda.Syntax.Concrete as C
+import Agda.Syntax.Common
+import Agda.Utils.Pretty (Doc, render, pretty)
+
+import System.FilePath ((<.>))
+import Data.List
+import Data.Monoid
+import Data.Function
+import qualified Data.Map as Map
+
+---------------------------------------------------------------
+
+-- | Constructs the HTML displaying the code.
+
+code'
+    :: (AreaID -> ResID -> Stmt ())
+    -> AgdaCode         -- ^ The contents of the module.
+    -> CompressedFile -- ^ Highlighting information.
+    -> Memo Html
+code' giveCode (unAgdaCode -> contents) info
+    = fmap mconcat
+    . mapM (\cs -> case cs of
+              (mi, (pos, _)) : _ -> annotate pos (maybe mempty id mi) (map (snd . snd) cs)
+              []                 -> error "__IMPOSSIBLE__"
+          )
+    . groupBy ((==) `on` fst)
+    . map (\(pos, c) -> (Map.lookup pos infoMap, (pos, c)))
+    . zip [1..]
+    $ contents
+  where
+    infoMap = toMap (decompress info)
+
+    getHole "?" = Just ""
+    getHole ('{':'!':cs)
+        | ('}':'!':cs') <- reverse cs
+        = Just $ reverse cs'
+    getHole _ = Nothing
+
+    annotate :: Integer -> MetaInfo -> String -> Memo Html
+    annotate pos mi s
+        | Just h <- getHole s -- = stringToHtml "HOLE"
+        = do
+            (i2, thediv_) <- thediv'
+            (i1, tar) <- textarea' 30 1
+            return $
+                thediv_ [] <<
+                    [ tar [] << h
+                    , br
+                    , button' "Give" (giveCode i1 i2)
+                    ]
+{-
+                ! [ theclass "interpreter"
+                  , thetype "text"
+                  , size $ show $ 3 + length h -- limit
+                  , maxlength 1000
+            --          , identifier $ "tarea" ++ i
+                  , value h -- $ if prompt == 'R' then "" else exp
+                  ]
+-}
+    annotate pos mi s
+        = return $ anchor ! attributes << stringToHtml s
+      where
+        attributes
+          = [name (show pos)]
+          ++ maybe [] link (definitionSite mi)
+          ++ (case classes of
+            [] -> []
+            cs -> [theclass $ unwords cs])
+
+        classes
+          =  maybe [] noteClasses (note mi)
+          ++ otherAspectClasses (otherAspects mi)
+          ++ maybe [] aspectClasses (aspect mi)
+
+        aspectClasses (Name mKind op) = kindClass ++ opClass
+          where
+            kindClass = maybe [] ((: []) . showKind) mKind
+
+            showKind (Constructor Inductive)   = "InductiveConstructor"
+            showKind (Constructor CoInductive) = "CoinductiveConstructor"
+            showKind k                         = show k
+
+            opClass = if op then ["Operator"] else []
+        aspectClasses a = [show a]
+
+        otherAspectClasses = map show
+
+        -- Notes are not included.
+        noteClasses s = []
+
+        link (m, pos) = [href $ modToFile m ++ "#" ++ show pos]
+          where
+            modToFile :: C.TopLevelModuleName -> FilePath
+            modToFile m = render (pretty m) <.> "xml"
+
+
+---------------------------------------------------------------
+{-
+instance IsString Html where
+    fromString = toHtml :: String -> Html
+-}
+showR :: Response -> Maybe Html
+showR (Resp_Status s) = Just $ ("checked: " :: String) +++ show (sChecked s)
+showR (Resp_DisplayInfo x) = Just $ showD x --a ++ " :displayinfo: " ++ b
+showR (Resp_RunningInfo i x) = Just $ "runninginfo: " +++ show i +++ x
+showR Resp_ClearRunningInfo = Just $ toHtml "clearRunningInfo"
+--showR (Resp_HighlightingInfo h) = "highlightingInfo: " ++ show h
+--showR (Resp_UpdateHighlighting (a,b)) = "highlighting: " ++ show (a,b)
+showR (Resp_JumpToError f i) = Just $ "jumpToError" +++ f +++ show i
+showR (Resp_InteractionPoints is) = Just $ "ipoints: " +++ show is
+showR (Resp_GiveAction i s) = Just $ "give: " +++ show i +++ showG s
+showR (Resp_MakeCaseAction ss) = Just $ "caseaction: " +++  ss
+showR (Resp_MakeCase s ss) = Just $ "case: " +++ s +++  ss
+showR (Resp_SolveAll x) = Just $ "solveAll: " +++ show x
+showR _ = Nothing
+
+instance HTML Doc where
+    toHtml = toHtml . render
+
+showG :: GiveResult -> Html
+showG (Give_String s) = toHtml s
+showG Give_Paren = toHtml "give paren"
+showG Give_NoParen = toHtml "give no paren"
+
+showD :: DisplayInfo -> Html
+showD x = case x of
+   Info_CompilationOk -> toHtml "compilation ok"
+   Info_Constraints s -> "constraints:" +++ s
+   Info_AllGoals s -> "all goals:" +++ s
+   Info_Error s -> "error:" +++ s
+   Info_Intro d -> "intro:" +++ d
+   Info_Auto s -> "auto:" +++ s
+   Info_ModuleContents d -> "module contents:" +++ d
+   Info_NormalForm d -> "normal form:" +++ d
+   Info_GoalType d -> "goal type:" +++ d
+   Info_CurrentGoal d -> "current goal:" +++ d
+   Info_InferredType d -> "inferred type:" +++ d
+   Info_Context d -> "context:" +++ d
+
+
diff --git a/JS.hs b/JS.hs
new file mode 100644
--- /dev/null
+++ b/JS.hs
@@ -0,0 +1,76 @@
+-- An interface to construct Exp, Stmt and Block data
+--    (later: dedicated data types)
+
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE EmptyDataDecls #-}
+
+module JS
+    ( toExp
+    , Exp
+    , Stmt
+    , setInnerHtml
+    , getAgdaCode
+    , button'
+    ) where
+
+import Param
+import Memo
+
+import Language.HJavaScript.Syntax
+import Text.XHtml.Strict (form, action)
+
+----------- type tags
+
+data JIO a
+data XML        -- for inner use
+data Document   -- for inner use
+
+-----------
+
+instance JType (JIO a) where
+instance JType XML where
+instance JType Html where
+
+instance IsExp Html HtmlStr where
+    toExp = toExp . htmlStr
+
+---------------
+
+getAgdaCode :: Exp AreaID -> Exp AgdaCode
+getAgdaCode = value_ . getElem
+
+getElem :: Exp AreaID -> Exp XML
+getElem = JCall $ JDeref document "getElementById"
+
+value_ :: Exp XML -> Exp AgdaCode
+value_ x = JDeref (Record_ x) "value"
+
+setInnerHtml :: Exp ResID -> Exp HtmlStr -> Exp HtmlStr
+setInnerHtml x y = JAssign (innerHtml_ x) y
+
+innerHtml_ :: Exp ResID -> Var HtmlStr
+innerHtml_ = innerHtml . getElem'
+
+getElem' :: Exp ResID -> Exp XML
+getElem' = JCall $ JDeref document "getElementById"
+
+innerHtml :: Exp XML -> Var HtmlStr
+innerHtml y = JDerefVar (Record_ y) "innerHTML"
+
+---------------- for inner use
+
+data Record_ a = Record_ (Exp a)
+
+instance Show (Record_ a) where show (Record_ x) = show x
+instance IsDeref (Record_ a)
+
+document :: Record_ Document
+document = Record_ $ JConst "document"
+
+button' :: String -> Stmt () -> Html
+button' title ac = form
+        ! [ action $ "javascript:" ++ show ac
+          ] << input ! [thetype "submit", value title]
+
+
diff --git a/JSDict.hs b/JSDict.hs
new file mode 100644
--- /dev/null
+++ b/JSDict.hs
@@ -0,0 +1,202 @@
+-- The JSDict data type and JSDictM monad
+
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module JSDict
+    ( JSDictM
+    , shareFun
+    , buildFun2
+    , buildStmt2
+    , buildStmt3
+    , newSM
+    , expStmt
+    , Def (..)
+    , runJSDictM
+    ) where
+
+import Param
+import JS
+import Memo
+
+import Language.HJavaScript.Syntax
+
+import Control.Monad.Identity
+import Control.Monad.Trans
+import Control.Monad.Trans.Writer
+import Control.Monad.Trans.State
+
+---------------------------------------------------------------
+
+
+data Def where
+    SMDef :: String -> {-n :-}Int -> ([String]{-Vec n String-} -> Memo String) -> Def
+    JSDef :: String -> Def
+
+type JSDictM = WriterT [Def] (StateT Int Identity)
+
+runJSDictM :: JSDictM a -> ((a, [Def]), Int)
+runJSDictM = runIdentity . flip runStateT (1 :: Int) . runWriterT
+
+data JSM x r where
+    Ret :: r -> JSM () r
+    Bind :: JSM () k -> (k -> JSM x r) -> JSM x r
+    VDA :: Exp t -> JSM () (Exp t)
+    ES :: Exp t -> JSM () ()
+
+type JSMB r = JSM r ()
+
+instance Monad (JSM ()) where
+    return = Ret
+    (>>=) = Bind
+
+expStmt :: Exp t -> JSM () ()
+expStmt = ES
+
+runJSM :: JSM r () -> JSDictM (Block r)
+runJSM = fmap fst . runJSM'
+
+infixl 1 |+|
+
+(|+|) :: forall t. Block () -> Stmt t -> Block t
+(|+|) = Sequence
+
+
+runJSM' :: JSM r a -> JSDictM (Block r, a)
+runJSM' (Ret r) = return (EmptyBlock, r)
+runJSM' (VDA e) = do
+    i <- newId
+    let v = 'd': i
+    return (EmptyBlock |+| VarDeclAssign v e, JConst v)
+runJSM' (ES e) =
+    return (EmptyBlock |+| ExpStmt e, ())
+runJSM' (Bind m f) = do
+    (a, x) <- runJSM' m
+    (b, y) <- runJSM' $ f x
+    return (a .+ b, y)
+
+(.+) :: Block () -> Block a -> Block a
+a .+ EmptyBlock = a
+a .+ Sequence b s = Sequence (a .+ b) s
+
+
+newId :: JSDictM String
+newId = do
+    i <- lift get
+    lift $ put $ i + 1
+    return $ show i
+
+newVar :: JSDictM (Var a)
+newVar = fmap (JParam . ('v':)) newId
+
+newFunName :: JSDictM String
+newFunName = fmap ('f':) newId
+
+
+tellJS :: (Show a) => a -> JSDictM ()
+tellJS f = tell [JSDef $ show f]
+
+tellSM :: String -> Int -> ([String] -> Memo String) -> JSDictM ()
+tellSM name i f = tell [SMDef name i f]
+
+getPre :: Exp String -> Exp (String -> ()) -> Stmt ()
+getPre = curry $
+        ExpStmt .
+--        JI .
+        JCall (JConst "getPre")
+
+infixr 5 `strPlus`
+
+strPlus :: Exp String -> Exp String -> Exp String
+strPlus x y = JBinOp x Plus y
+
+(|=|) :: String -> Exp String -> Exp String
+t |=| x = JString (t ++ "=") `strPlus` encodeURIComponent x
+
+encodeURIComponent :: Exp String -> Exp String
+encodeURIComponent = JCall $ JConst "encodeURIComponent"
+
+infixr 3 |&|
+
+(|&|) :: Exp String -> Exp String -> Exp String
+a |&| b = a `strPlus` JString "&" `strPlus` b
+
+
+newSM
+    :: forall t1 t2 t3 a
+    . (FromString t1, FromString t2, ToString t3)
+    => (t1 -> t2 -> Memo t3)
+    -> JSDictM ( Exp t1
+              -> Exp t2
+              -> (Exp t3 -> Exp a)
+              -> Exp ())
+newSM body = do
+    name <- newFunName
+    (w1 :: Var String) <- newVar
+    (w2 :: Var String) <- newVar
+    (w3 :: Var (String -> ())) <- newVar
+    (v1 :: Var t3) <- newVar
+    tellJS $ JFunction (Just name) (w1, w2, w3)
+                  $ EmptyBlock
+                |+| getPre ( "sm" |=| JString name
+                         |&| "v1" |=| val w1
+                         |&| "v2" |=| val w2)
+                    (val w3)
+
+    tellSM name 2 $ \[x, y] -> fmap ts $ body (fs x) (fs y)
+    return $ \w1 w2 w3f
+        -> JCall (JConst name)
+            (w1, w2, JFunction Nothing v1
+                        $ EmptyBlock
+                      |+| ExpStmt (w3f $ val v1))
+
+
+
+buildFun :: forall t r . ParamType t => (Exp t -> Block r) -> JSDictM (Exp t -> Exp r)
+buildFun body = do
+    name <- newFunName
+    v <- newVar
+    tellJS $ JFunction (Just name) v $ body $ val v
+    return $ JCall $ JConst name
+
+shareFun :: forall t r . ParamType t => (Exp t -> Exp r) -> JSDictM (Exp t -> Exp r)
+shareFun f = buildFun $ Sequence EmptyBlock . Return . f
+
+buildFun2 :: forall t1 t2 r . ParamType (t1,t2)
+    => (Exp t1 -> Exp t2 -> JSMB r)
+    -> JSDictM (Exp t1 -> Exp t2 -> Exp r)
+buildFun2 body = do
+    name <- newFunName
+    v1 <- newVar
+    v2 <- newVar
+    b <- runJSM $ body (val v1) (val v2)
+    tellJS $ JFunction (Just name) (v1,v2) b
+
+    return $ \v1 v2 -> JCall (JConst name) (v1,v2)
+
+buildStmt2 :: forall t1 t2 r . ParamType (t1,t2)
+    => (Exp t1 -> Exp t2 -> JSMB r)
+    -> JSDictM (Exp t1 -> Exp t2 -> Stmt ())
+buildStmt2 f = fmap (\f a b -> ExpStmt $ f a b) $ buildFun2 f
+
+buildFun3 :: forall t1 t2 t3 r . ParamType (t1,t2,t3)
+    => (Exp t1 -> Exp t2 -> Exp t3 -> JSMB r)
+    -> JSDictM (Exp t1 -> Exp t2 -> Exp t3 -> Exp r)
+buildFun3 body = do
+    name <- newFunName
+    v1 <- newVar
+    v2 <- newVar
+    v3 <- newVar
+    b <- runJSM $ body (val v1) (val v2) (val v3)
+    tellJS $ JFunction (Just name) (v1,v2,v3) b
+    return $ \v1 v2 v3 -> JCall (JConst name) (v1,v2,v3)
+
+buildStmt3 :: forall t1 t2 t3 r . ParamType (t1,t2,t3)
+    => (Exp t1 -> Exp t2 -> Exp t3 -> JSMB ())
+    -> JSDictM (Exp t1 -> Exp t2 -> Exp t3 -> Stmt ())
+buildStmt3 f = fmap (\f t1 t2 t3 -> ExpStmt $ f t1 t2 t3) $ buildFun3 f
+
+
+
diff --git a/JSDictDef.hs b/JSDictDef.hs
new file mode 100644
--- /dev/null
+++ b/JSDictDef.hs
@@ -0,0 +1,100 @@
+--   JSDict implementation
+
+{-# LANGUAGE RecursiveDo #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module JSDictDef
+    ( jsDictM
+    , Common
+    ) where
+
+import JS
+import Memo
+import JSDict
+import Html
+
+import AgdaInterface
+
+import Data.Monoid
+import Data.Maybe
+import qualified Data.List as List
+
+---------------------------------------------------------------
+
+type Common = CodePath -> AgdaCode -> Memo Html
+
+jsDictM :: [FilePath] -> JSDictM Common
+jsDictM includedirs = do 
+
+    getValue <- shareFun getAgdaCode
+
+    setValue <- buildStmt2 $ \x y -> expStmt $ setInnerHtml x y
+
+    rec
+        getCode_ <- newSM $ \filepath code -> do
+            writeAgdaFile filepath code
+            fmap htmlStr $ common filepath code
+
+        getCode <- buildStmt3 $ \filepath (fr :: Exp AreaID) (t :: Exp ResID) ->
+            expStmt $ getCode_ filepath (getValue fr) $ setInnerHtml t
+
+        giveCode__ <- newSM $ \filepath code -> do
+            let ii = InteractionId 0
+            rs <- giveCmd filepath ii (Range []) code
+            case [ s | Resp_GiveAction i s <- rs, i == ii ] of
+                [Give_String s] -> do
+                    writeAgdaFileGive filepath s
+                    return $ htmlStr $ toHtml s
+                _ -> do
+                        (i2, thediv_) <- thediv'
+                        (i1, tar) <- textarea' 30 1
+                        return $ htmlStr $ 
+                            thediv_ [] <<
+                                [ tar [] << unAgdaCode code
+                                , br
+                                , button' "Give" (giveCode filepath i1 i2)
+                                , br
+                                , err rs
+                                ]
+
+        giveCode_ <- buildStmt3 $ \filepath (fr :: Exp AreaID) (t :: Exp ResID) ->
+            expStmt $ giveCode__ filepath (getValue fr) $ setInnerHtml t
+
+        let giveCode filepath i1 i2 = giveCode_ (toExp filepath) (toExp i1) (toExp i2)
+
+        let common :: Common
+            common filepath code = do
+                i2 <- getMainDiv filepath
+                (i1, tar) <- textarea' 80 10
+                let
+                    high rs = case [(x,y) | Resp_HighlightingInfo x y <- rs] of
+
+                        [] -> return
+                                $ showEdit
+                                +++ err rs
+                        fp -> do
+                            c <- code' (giveCode filepath) code $ mconcat $ map fst fp
+                            return
+                                $ c
+--                                +++ err rs
+--                                +++ br 
+                                +++ button' "Edit" (setValue (toExp i2) $ toExp showEdit)
+
+
+                    showEdit
+                        = (tar [] << agdaCodeHtml code)
+                        +++ br
+                        +++ (button' "Check" $ getCode (toExp filepath) (toExp i1) (toExp i2))
+
+                loadCmd includedirs filepath >>= high
+
+    return common
+
+err :: [Response] -> Html
+err = mconcat
+    . List.intersperse br
+--    . map stringToHtml
+--    . filter (not . null)
+    . catMaybes
+    . map showR
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,31 @@
+Copyright Péter Diviánszky 2012-2013
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of the authors nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
diff --git a/Main.hs b/Main.hs
new file mode 100644
--- /dev/null
+++ b/Main.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE NamedFieldPuns #-}
+
+module Main
+    ( main
+    ) where
+
+import Args
+import Memo
+import JSDict
+import JSDictDef
+import Standalone
+
+import Snap.Core
+import Snap.Http.Server (httpServe)
+import Snap.Http.Server.Config
+import Snap.Util.FileServe (getSafePath, serveDirectoryWith, simpleDirectoryConfig)
+
+import Data.ByteString.UTF8 (fromString, toString)
+
+import System.FilePath
+
+import Control.Applicative ((<|>))
+import Control.Monad
+import Control.Monad.Trans
+
+---------------------------------------------------------------
+
+main :: IO ()
+main = getArgs >>= mainWithArgs
+
+mainWithArgs :: Args -> IO ()
+mainWithArgs (Args {sourcedir, port, datadir, includedir, logdir}) = do
+    putStrLn $ "Working directory: " ++ show sourcedir
+    putStrLn $ "Include directories: " ++ show includedir
+    let -- includedirs = ["", "/home/divip/share/agda/std-lib/src"]
+
+        templatepath = datadir </> "agda.template"
+        jsfile = datadir </> "common.js"
+
+    let ((common, definitions), idC) = runJSDictM $ jsDictM includedir
+
+    runMemo <- initMemo idC
+
+    ht <- liftIO $ readFile templatepath
+
+    let serveHtml = do
+            p <- getSafePath
+            guard $ takeExtension p `elem` [".xml"]
+            return $ standalone ht common sourcedir $ dropExtension p
+
+        runSM name i fun = do
+            mn <- getParam' "sm"
+            guard $ name == mn
+            fmap fun $ mapM (getParam' . ('v':) . show) [1..i]
+
+    writeFile jsfile $ unlines [x | JSDef x <- definitions]
+
+    httpServe
+
+        ( setPort port
+        . setAccessLog (if null logdir then ConfigNoLog else ConfigFileLog (logdir </> "access.log"))
+        . setErrorLog  (if null logdir then ConfigNoLog else ConfigFileLog (logdir </> "error.log"))
+        $ emptyConfig
+        )
+
+        (   method GET
+            (   (writeBS . fromString =<< runMemo =<< serveHtml)
+            <|> serveDirectoryWith simpleDirectoryConfig datadir
+            <|> serveDirectoryWith simpleDirectoryConfig sourcedir
+            )
+        <|> method POST
+            (   ( writeBS . fromString =<< runMemo =<<
+                    msum [runSM name i fun | SMDef name i fun <- definitions]
+                )
+            <|> writeBS "Invalid post request"
+            )
+        <|> writeBS "Not found. Try to find X.xml for example."
+        )
+
+getParam' :: String -> Snap String
+getParam' t = do
+    Just x <- getParam $ fromString t
+    return $ toString x
+
+
+
diff --git a/Memo.hs b/Memo.hs
new file mode 100644
--- /dev/null
+++ b/Memo.hs
@@ -0,0 +1,257 @@
+-- An interface to construct Memo actions
+--    type Memo = StateT MemoState Snap
+--    (later: newtype)
+
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Memo
+    ( Memo
+    , initMemo
+    , loadCmd
+    , giveCmd
+    , newMemoId     -- for inner use
+    , setMainDiv
+    , getMainDiv
+    , loadAgdaFile
+    , writeAgdaFile
+    , writeAgdaFileGive
+
+    , ResID
+    , AreaID
+    , HtmlStr
+    , CodePath
+    , AgdaCode (unAgdaCode)
+    , agdaCodeHtml
+
+    , Html, HTML
+    , toHtml
+    , textarea', thediv'
+    , indent
+    , stringToHtml'
+    , (+++), br, (<<), rows, cols
+    , stringToHtml, (!), thediv, theclass, pre
+    , htmlStr
+    , input, thetype, size, maxlength, value, anchor, name, href
+    , floatRight
+    ) where
+
+import Param
+
+import Text.XHtml.Strict
+
+import Snap.Core (Snap)
+
+import AgdaInterface
+
+import Control.Concurrent.MVar
+import Control.Monad
+import Control.Monad.Trans
+import Control.Monad.Trans.State
+import Control.Monad.Trans.Reader
+import Data.List
+--import Data.Maybe
+import Data.Monoid
+import System.FilePath
+import System.Directory
+
+---------------------------------------------------------------
+
+type IState = (ResID, InteractionState)
+
+data SR = SR
+    { sr_filePath :: CodePath
+    , _sr_is       :: Maybe IState
+    }
+
+type MemoState = (MVar [SR], MVar Int)
+
+newtype Memo a
+    = Memo (ReaderT MemoState Snap a)
+        deriving (Functor, Monad, MonadIO)
+
+initMemo :: Int -> IO (Memo m -> Snap m)
+initMemo i = do
+    state <- liftM2 (,) (newMVar []) (newMVar i)
+    return $ \(Memo m) -> runReaderT m state
+
+newMemoId :: Memo String
+newMemoId = Memo $ ReaderT $ \(_,v) -> do
+    i <- liftIO $ takeMVar v
+    liftIO $ putMVar v $! i + 1
+    return $ 'm' : show i
+
+
+--initState :: FilePath -> 
+
+getState_ :: CodePath -> Memo IState
+getState_ fp = Memo $ ReaderT $ \(state, _) -> do
+    Just s <- liftIO $ modifyMVar state $ \xs -> return $ do
+        case [x | x <- xs, sr_filePath x == fp] of
+            [SR _ s@(Just _)] -> (SR fp Nothing : dele fp xs, s)
+            [] -> (SR fp Nothing : xs, Just (ResID "", initState)) --Just (stringToHtml "Empty", "", initState))
+    return s
+
+saveState_ :: CodePath -> IState -> Memo ()
+saveState_ fp s = Memo $ ReaderT $ \(state, _) ->
+    liftIO $ modifyMVar_ state $ \xs -> do
+        case [x | x <- xs, sr_filePath x == fp] of
+            [SR _ Nothing] -> return $ SR fp (Just s) : dele fp xs
+--            [] -> return $ SR fp (Just s) : xs
+
+
+newtype ResID = ResID { unResID :: String }
+
+instance JType ResID
+
+instance IsExp ResID ResID where
+    toExp = jconst . unResID
+
+
+newtype CodePath = CodePath { unCodePath :: String }
+    deriving Eq
+
+instance JType CodePath
+
+instance FromString CodePath where fs = CodePath
+
+instance IsExp CodePath CodePath where
+    toExp = jconst . unCodePath
+
+
+setMainDiv :: CodePath -> ResID -> Memo ()
+setMainDiv fp s = do
+    (_, st) <- getState_ fp
+    saveState_ fp (s, st)
+
+getMainDiv :: CodePath -> Memo ResID
+getMainDiv fp = do
+    (s, st) <- getState_ fp
+    saveState_ fp (s, st)
+    return s
+
+dele :: CodePath -> [SR] -> [SR]
+dele fp = filter ((/=fp) . sr_filePath)
+
+tcmAction :: CodePath -> Interaction -> Memo [Response]
+tcmAction filepath action = do
+    (md, st) <- getState_ filepath
+    (rs, endstate) <- liftIO $ runStateT (tcmAction_ (unCodePath filepath) action) st
+    saveState_ filepath (md, {-fromMaybe st-} endstate)
+    return rs
+
+
+loadCmd :: [FilePath] -> CodePath -> Memo [Response]
+loadCmd includedirs filepath
+    = tcmAction filepath $ Cmd_load (unCodePath filepath) includedirs
+
+giveCmd :: CodePath -> InteractionId -> Range -> AgdaCode -> Memo [Response]
+giveCmd filepath ii r c
+    = tcmAction filepath $ Cmd_give ii r (unAgdaCode c)
+
+loadAgdaFile
+  :: FilePath
+  -> FilePath
+  -> Memo (AgdaCode, String, CodePath)
+loadAgdaFile workdir inp__ = liftIO $ do
+    b <- doesFileExist inp
+    when (not b) $ writeFile inp $ unwords ["module", inp', "where"] ++ "\n\n\n"
+    x <- readFile inp
+    return (AgdaCode x, inp', CodePath inp)
+  where
+    inp = workdir </> inp__ <.> "agda"
+    inp' = map repl inp__
+
+    repl '/' = '.'
+    repl c = c
+
+writeAgdaFile :: CodePath -> AgdaCode -> Memo ()
+writeAgdaFile filepath code
+    = liftIO $ writeFile (unCodePath filepath) (unAgdaCode code)
+
+writeAgdaFileGive :: CodePath -> String -> Memo ()
+writeAgdaFileGive filepath code
+    = liftIO $ do
+        x <- readFile (unCodePath filepath)
+        length x `seq` return ()
+        writeFile (unCodePath filepath) $ repHole code x
+  where
+    repHole x ('?':c22) = x ++ c22
+    repHole x ('{':'!':c2) = x ++ c22
+      where
+        (_, c22) = split "!}" c2
+    repHole x (c:cs) = c: repHole x cs
+
+split :: [Char] -> [Char] -> ([Char], [Char])
+split a b = (reverse c, d) where
+    (c,d) = split' a b
+    split' s s' | isPrefixOf s s' = ("", drop (length s) s')
+    split' s (c:cs) = (c:x, y)
+      where
+        (x,y) = split s cs
+
+
+---------------
+
+newtype AreaID = AreaID { unAreaID :: String }
+
+instance JType AreaID
+
+instance IsExp AreaID AreaID where
+    toExp = jconst . unAreaID
+
+
+newtype HtmlStr = HtmlStr { unHtmlStr :: String }
+
+instance IsExp HtmlStr HtmlStr where
+    toExp = jconst . unHtmlStr
+
+instance JType HtmlStr
+
+instance ToString HtmlStr where ts = unHtmlStr
+
+-----
+
+textarea' :: Int -> Int -> Memo (AreaID, [HtmlAttr] -> Html -> Html)
+textarea' c r = do
+    i <- newMemoId    
+    return (AreaID i, \xs -> textarea ! ([identifier i, cols (show c), rows (show r) ] ++ xs))
+
+floatRight :: HtmlAttr
+floatRight = strAttr "style" "float:right"
+
+thediv' :: Memo (ResID, [HtmlAttr] -> Html -> Html)
+thediv' = do
+    i <- newMemoId    
+    return (ResID i, \xs -> thediv ! (identifier i : xs))
+
+htmlStr :: Html -> HtmlStr
+htmlStr = HtmlStr . showHtmlFragment
+
+indent :: HTML a => a -> Html
+indent x = thediv ! [ theclass "indent" ]  << x
+
+lines' :: String -> [String]
+lines' [] = []
+lines' ('\n':cs) = []: lines' cs
+lines' (c:cs) = add c $ lines' cs
+  where
+    add x (xs:xss) = (x:xs):xss
+    add x [] = [[x]]
+
+stringToHtml' :: String -> Html
+stringToHtml' = mconcat . intersperse br . map stringToHtml . lines'
+
+
+------
+
+newtype AgdaCode = AgdaCode { unAgdaCode :: String }
+
+instance JType AgdaCode
+
+instance FromString AgdaCode where fs = AgdaCode
+
+agdaCodeHtml :: AgdaCode -> Html
+agdaCodeHtml = toHtml . unAgdaCode
+
+
diff --git a/Param.hs b/Param.hs
new file mode 100644
--- /dev/null
+++ b/Param.hs
@@ -0,0 +1,23 @@
+
+module Param
+    ( FromString (..)
+    , ToString (..)
+    , jconst
+    , IsExp (..)
+    , JType
+    ) where
+
+import Language.HJavaScript.Syntax
+
+--------------
+
+class JType a => FromString a where
+    fs :: String -> a
+
+class ParamType a => ToString a where
+    ts :: a -> String
+
+jconst :: String -> Exp a
+jconst = JConst . show . toExp
+
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/Standalone.hs b/Standalone.hs
new file mode 100644
--- /dev/null
+++ b/Standalone.hs
@@ -0,0 +1,48 @@
+-- getResponse :: url -> params -> SnapState FullHtml
+
+
+module Standalone
+    ( standalone
+    ) where
+
+import Memo
+import JSDictDef
+
+import Text.XHtml.Strict (showHtmlFragment)
+import Text.Pandoc
+
+---------------------------------------------------------------
+
+standalone
+    :: String
+    -> Common
+    -> FilePath
+    -> FilePath
+    -> Memo String
+standalone ht common workdir filepath = do
+
+    (filecont, inp', inp) <- loadAgdaFile workdir filepath
+
+    (i2, thediv_) <- thediv'
+
+    setMainDiv inp i2
+
+    res <- fmap (\x -> pre << thediv_ [theclass "answer"] << x)
+            $ common inp filecont
+
+    let
+        meta = Meta
+            { docTitle = [Str inp']
+            , docAuthors = []
+            , docDate = []
+            }
+
+    return $ writeHtmlString `flip` Pandoc meta [ RawBlock "html" $ showHtmlFragment res ]
+      $ def
+        { writerStandalone      = True
+        , writerTableOfContents = True
+        , writerSectionDivs     = True
+        , writerTemplate        = ht
+        }
+
+
diff --git a/agda-server.cabal b/agda-server.cabal
new file mode 100644
--- /dev/null
+++ b/agda-server.cabal
@@ -0,0 +1,54 @@
+name:               agda-server
+version:            0.1
+category:           Dependent types
+synopsis:           Http server for Agda (prototype)
+description:
+    @agda-server@ serves agda files as XML files.
+    .
+    Usage: Run @agda-server@ (see --help for command line options). Then open a browser
+    with @localhost:8001//X.xml@ (or similar).
+    .
+    Supported features: Type checking (whole module), links between modules (but not between library modules), basic support for holes.
+stability:          experimental
+license:            BSD3
+license-file:       LICENSE
+author:             Péter Diviánszky
+maintainer:         divipp@gmail.com
+cabal-version:      >=1.6
+build-type:         Simple
+data-files:
+                    copy/*.css,
+                    copy/*.js,
+                    copy/*.template,
+                    copy/icon.ico
+
+Executable agda-server
+  GHC-Options:      -threaded -rtsopts -Wall -fwarn-tabs -fno-warn-incomplete-patterns -fno-warn-type-defaults -fno-warn-unused-matches -fno-warn-name-shadowing
+  Main-is:
+                    Main.hs
+  Other-modules:
+                    AgdaInterface
+                    Args
+                    Html
+                    JSDictDef
+                    JSDict
+                    JS
+                    Memo
+                    Param
+                    Standalone
+  Build-Depends:
+                    base < 5
+                  , containers
+                  , transformers
+                  , mtl
+                  , filepath
+                  , directory
+                  , cmdargs
+                  , utf8-string
+                  , xhtml
+                  , HJavaScript
+                  , pandoc
+                  , snap-core
+                  , snap-server
+                  , Agda >= 2.3.3
+
diff --git a/copy/Agda.css b/copy/Agda.css
new file mode 100644
--- /dev/null
+++ b/copy/Agda.css
@@ -0,0 +1,31 @@
+/* Aspects. */
+.Comment       { color: #B22222 }
+.Keyword       { color: #CD6600 }
+.String        { color: #B22222 }
+.Number        { color: #A020F0 }
+.Symbol        { color: #404040 }
+.PrimitiveType { color: #0000CD }
+.Operator      {}
+
+/* NameKinds. */
+.Bound                  { color: black   }
+.InductiveConstructor   { color: #008B00 }
+.CoinductiveConstructor { color: #8B7500 }
+.Datatype               { color: #0000CD }
+.Field                  { color: #EE1289 }
+.Function               { color: #0000CD }
+.Module                 { color: #A020F0 }
+.Postulate              { color: #0000CD }
+.Primitive              { color: #0000CD }
+.Record                 { color: #0000CD }
+
+/* OtherAspects. */
+.DottedPattern      {}
+.UnsolvedMeta       { color: black; background: yellow         }
+.TerminationProblem { color: black; background: #FFA07A        }
+.IncompletePattern  { color: black; background: #F5DEB3        }
+.Error              { color: red;   text-decoration: underline }
+
+/* Standard attributes. */
+a { text-decoration: none }
+a[href]:hover { background-color: #B4EEB4 }
diff --git a/copy/agda.template b/copy/agda.template
new file mode 100644
--- /dev/null
+++ b/copy/agda.template
@@ -0,0 +1,22 @@
+<?xml version="1.0" encoding="utf-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en"> 
+<head>
+<title>$pagetitle$</title>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+<meta name="generator" content="pandoc" />
+<link rel="shortcut icon" href="icon.ico" />
+<script src="common_en.js" charset="utf-8" type="text/javascript"></script> 
+<script src="common.js" charset="utf-8" type="text/javascript"></script> 
+<link rel="stylesheet" href="common.css" type="text/css" />
+<link rel="stylesheet" href="Agda.css" type="text/css" />
+</head>
+<body onload="javascript:resetForms(); javascript:slidy_init();">
+<div><h1 class="cover">$title$</h1>
+<div id="info"></div>
+$toc$
+</div>
+$body$
+</body>
+</html>
+
diff --git a/copy/common.css b/copy/common.css
new file mode 100644
--- /dev/null
+++ b/copy/common.css
@@ -0,0 +1,205 @@
+
+/* slides */
+
+body.single_slide > * { display: none; visibility: hidden }
+body.single_slide .current { display: block; visibility: visible }
+body.single_slide div#TOC { display: none; visibility: hidden }
+body.single_slide div.handout { display: none; visibility: hidden }
+body.single_slide div#lang { display: block; visibility: visible }
+
+
+/* padding */
+
+body {
+  margin: auto;
+  padding: 1em 1em 1em 1em;
+  max-width: 50em; 
+  line-height: 130%;
+  background-color: white;
+  color: black;
+}
+
+h1 {
+  padding-top: 1.5em;
+}
+
+h2 {
+  padding-top: 1em;
+}
+
+h3 {
+  padding-top: 0.5em;
+}
+
+h1.cover {
+  padding-top: 3em;
+  padding-bottom: 2em;
+  text-align: center;
+  line-height: normal;
+}
+
+hr {
+  height: 10px;
+}
+
+
+/* margin */
+
+div.indent, pre, table {
+  margin-left: 5%;
+  width: 95%;
+}
+
+div.indent, pre {
+  margin-top: 0.5em;
+  margin-bottom: 0.5em;
+}
+
+pre.normal {
+  margin: 0;
+  width: auto;
+}
+
+
+div.indent input {
+  margin-bottom: 0.5em;
+}
+
+input, textarea {
+  margin: 0;
+}
+
+
+/* border */
+
+h1, h2, h3 { 
+  border-bottom: 1px dotted black;
+}
+
+h1.cover, input, textarea, hr {
+  border-style: none;
+}
+
+
+/* font sizes */
+
+h1              { font-size: 130%; }
+h1.cover        { font-size: 200%; }
+h2              { font-size: 110%; }
+input, textarea { font-size: 100%; } /* monospace correction */
+
+
+/* font family, style, weight, text decoration */
+
+h1, h2, h3 {
+  font-weight: bold;
+}
+
+pre code, textarea, div.string {
+  font-family: monospace;
+  font-size: 130%;
+}
+
+pre.normal, pre.normal code, code, .error, input {
+  font-family: sans-serif;
+  font-size: 100%;
+}
+
+
+.wait {
+  font-style: italic;
+}
+
+a {
+  text-decoration: none;
+}
+
+
+
+div.serious {font-weight: bold;}
+div.info {color: gray;}
+
+
+/* colors other than highlighting */
+
+input           { background-color: #eeeeee; }
+textarea        { background-color: #ffffba; }
+hr              { background-color: #f5f0ee; }
+div.string span { background-color: yellow; }
+
+a               { color: #2a207a; }
+h1 a, h2 a, h3 a { color: black; }
+code            { color: red; }
+.wait           { color: gray; }
+.result         { color: green; }
+.type           { color: #0080ff; }
+.error          { color: #a030a0; }
+.comment        { color: gray; float: right; }
+
+
+/* misc */
+
+.result {
+  word-wrap: break-word;
+}
+
+p.caption {
+  display: none;
+}
+
+div#lang {
+  position:fixed;
+  z-index:1000;
+  right: 1%;
+  top: 1%;
+}
+
+div#info {
+  display: none;
+  position:fixed;
+  z-index:1000;
+  left: 40%;
+  width: 20%;
+  top: 40%;
+  height: 20%; 
+}
+
+.wait {
+  padding: 10px;
+  width: 8em;
+  border: 1px solid grey;
+}
+
+/*  search result colors  */
+
+code.search { color: black; }
+code.search b { color: gray; }
+
+.c0{background-color: #fcc;}
+.c1{background-color: #cfc;}
+.c2{background-color: #ccf;}
+.c3{background-color: #ffc;}
+.c4{background-color: #fcf;}
+.c5{background-color: #cff;}
+
+
+/*  highlighting css  */
+
+table.sourceCode, tr.sourceCode, td.lineNumbers, td.sourceCode, table.sourceCode 
+   { margin: 0; padding: 0; border: 0; vertical-align: baseline; border: none; }
+td.lineNumbers { border-right: 1px solid #AAAAAA; text-align: right; color: #AAAAAA; padding-right: 5px; padding-left: 5px; }
+td.sourceCode { padding-left: 5px; }
+pre.sourceCode span.kw { color: #007020; /* font-weight: bold; */ } 
+pre.sourceCode span.dt { color: #902000; }
+pre.sourceCode span.dv { color: #40a070; }
+pre.sourceCode span.bn { color: #40a070; }
+pre.sourceCode span.fl { color: #40a070; }
+pre.sourceCode span.ch { color: #4070a0; }
+pre.sourceCode span.st { color: #4070a0; }
+pre.sourceCode span.co { color: #60a0b0; /* font-style: italic; */ }
+pre.sourceCode span.ot { color: #007020; }
+pre.sourceCode span.al { color: red; /* font-weight: bold; */ }
+pre.sourceCode span.fu { color: #06287e; }
+pre.sourceCode span.re { }
+pre.sourceCode span.er { color: red; /* font-weight: bold; */ }
+
diff --git a/copy/common.js b/copy/common.js
new file mode 100644
--- /dev/null
+++ b/copy/common.js
@@ -0,0 +1,6 @@
+function f1(v2){return document.getElementById(v2).value;}
+function f3(v4,v5){document.getElementById(v4).innerHTML = v5;}
+function f6(v7,v8,v9){getPre('sm=' + encodeURIComponent('f6') + '&' + 'v1=' + encodeURIComponent(v7) + '&' + 'v2=' + encodeURIComponent(v8),v9);}
+function f11(v12,v13,v14){f6(v12,f1(v13),function (v10){document.getElementById(v14).innerHTML = v10;});}
+function f15(v16,v17,v18){getPre('sm=' + encodeURIComponent('f15') + '&' + 'v1=' + encodeURIComponent(v16) + '&' + 'v2=' + encodeURIComponent(v17),v18);}
+function f20(v21,v22,v23){f15(v21,f1(v22),function (v19){document.getElementById(v23).innerHTML = v19;});}
diff --git a/copy/common_en.js b/copy/common_en.js
new file mode 100644
--- /dev/null
+++ b/copy/common_en.js
@@ -0,0 +1,81 @@
+
+var waiting = 0;
+var waitingtimeout;
+
+function getPre(params, cont) {
+//    alert('get: ' + params);
+    var http = false;
+    if (window.XMLHttpRequest) { // Mozilla, Safari,...
+        http = new XMLHttpRequest();
+        if (http.overrideMimeType) {
+            http.overrideMimeType('text/html');
+        }
+    } else {
+        if (window.ActiveXObject) { // IE
+            try {
+                http = new ActiveXObject("Msxml2.XMLHTTP");
+            } catch (e) {
+                try {
+                    http = new ActiveXObject("Microsoft.XMLHTTP");
+                } catch (e) {}
+            }
+        }
+    }
+    if (!http) {
+        cont('<span class="error">Client error.</span>');
+    } else {
+
+//        alert('get ready: x ' );
+
+        if (waiting == 0) {
+            waitingtimeout = setTimeout("drawWarning(1);", 1000);
+        };
+        waiting = waiting + 1;
+
+        http.onreadystatechange = function () {
+            if (http.readyState == 4) {
+                waiting = waiting - 1;
+                if (waiting == 0) {
+                    clearTimeout(waitingtimeout);
+                    setTimeout("clearWarning();", 500);
+                };
+                cont(http.responseText);
+            }
+        }
+
+        http.open('POST', "exercise/", true);
+        http.setRequestHeader("Content-type", "application/x-www-form-urlencoded");
+        http.setRequestHeader("Content-length", params.length);
+        http.setRequestHeader("Connection", "close");
+        http.send(params);
+    }
+}
+
+//////////////////////////////////////////////////
+
+function drawWarning(n) {
+    var r="Waiting."; 
+    for (var a=0; a< n % 3; a++) r+='.';
+    document.getElementById('info').style.display = "block";
+    document.getElementById('info').innerHTML = '<div class="wait">' + r + '</div>';
+    waitingtimeout = setTimeout('drawWarning(' + (n+1) + ');', 500);
+}
+
+function clearWarning() {
+    document.getElementById('info').style.display = "none";
+    document.getElementById('info').innerHTML = "";
+}
+
+
+//////////////////////////////////////////////////
+
+function resetForms() {
+    var forms = document.getElementsByTagName("form");
+    for(var index=0;index<forms.length;index++) {
+        if (forms[index].className == 'resetinterpreter') { 
+            forms[index].reset(); 
+        }
+    }
+}
+
+
diff --git a/copy/icon.ico b/copy/icon.ico
new file mode 100644
Binary files /dev/null and b/copy/icon.ico differ
diff --git a/copy/slidy.js b/copy/slidy.js
new file mode 100644
--- /dev/null
+++ b/copy/slidy.js
@@ -0,0 +1,161 @@
+// after w3c slidy, http://www.w3.org/Talks/Tools/Slidy2/
+
+var slidy = {
+  key_wanted: false,
+  slide_number: 0, // integer slide count: 0, 1, 2, ...
+  view_all: true,  // true: view all slides + handouts
+
+  show_slide: function () {
+    window.scrollTo(0,0);
+    set_class(document.getElementsByTagName('body')[0].children[slidy.slide_number], "current");
+  },
+
+  switch_slide: function (event, n) {
+    if (slidy.view_all) {
+      return true;
+    } else {
+      var x = document.getElementsByTagName('body')[0].children;
+      if (n >= 0 && n < x.length && n != slidy.slide_number) {
+        set_class(x[slidy.slide_number], "");
+        slidy.slide_number = n;
+        slidy.show_slide();
+      }
+      return slidy.cancel(event);
+    }
+  },
+
+  // needed for Opera to inhibit default behavior
+  // since Opera delivers keyPress even if keyDown
+  // was cancelled
+  key_press: function (event) {
+    if (!event)
+      event = window.event;
+
+    if (!slidy.key_wanted)
+      return slidy.cancel(event);
+
+    return true;
+  },
+
+  //  See e.g. http://www.quirksmode.org/js/events/keys.html for keycodes
+  key_down: function (event) {
+    var key, target, tag;
+
+    slidy.key_wanted = true;
+
+    if (!event)
+      event = window.event;
+
+    // kludge around NS/IE differences 
+    if (window.event)
+    {
+      key = window.event.keyCode;
+      target = window.event.srcElement;
+    }
+    else if (event.which)
+    {
+      key = event.which;
+      target = event.target;
+    }
+    else
+      return true; // Yikes! unknown browser
+
+    // ignore event if key value is zero
+    // as for alt on Opera and Konqueror
+    if (!key)
+       return true;
+
+    if (slidy.special_element(target))
+      return true;
+
+    // check for concurrent control/command/alt key
+    // but are these only present on mouse events?
+    if (event.ctrlKey || event.altKey || event.metaKey)
+       return true;
+
+    if (key == 32 || key == 39) { // space bar, right arrow
+      slidy.switch_slide(event, slidy.slide_number + 1);
+    } else if (key == 37) { // left arrow
+      slidy.switch_slide(event, slidy.slide_number - 1);
+    } else if (key == 36) { // Home
+      slidy.switch_slide(event, 0);
+    } else if (key == 35) { // End
+      slidy.switch_slide(event, document.getElementsByTagName('body')[0].children.length - 1);
+    } else if (key == 65 && document.getElementsByTagName('body')[0].children.length > 3) {  // A
+
+        var x = document.getElementsByTagName('body')[0].children;
+
+        if (slidy.view_all) {
+          set_class(document.getElementsByTagName('body')[0], "single_slide");
+          // var y = 0; //yTop();
+          // slidy.slide_number = 0;
+          // while (findDiff(x[slidy.slide_number])[1] < 0
+          //       && slidy.slide_number < x.length - 1) {
+          //  slidy.slide_number += 1;
+          // }
+          slidy.show_slide();
+        } else {
+          set_class(document.getElementsByTagName('body')[0], "");
+          x[slidy.slide_number].scrollIntoView();
+          // set_class(x[slidy.slide_number], "");
+        }
+        slidy.view_all = !slidy.view_all;
+        return slidy.cancel(event);
+    }
+    return true;
+  },
+
+  special_element: function (e) {
+    var tag = e.nodeName.toLowerCase();
+
+    return e.onkeydown ||
+      e.onclick ||
+      tag == "a" ||
+      tag == "embed" ||
+      tag == "object" ||
+      tag == "video" ||
+      tag == "audio" ||
+      tag == "input" ||
+      tag == "textarea" ||
+      tag == "select" ||
+      tag == "option";
+  },
+
+  cancel: function (event) {
+    if (event)
+    {
+       event.cancel = true;
+       event.returnValue = false;
+
+      if (event.preventDefault)
+        event.preventDefault();
+    }
+
+    slidy.key_wanted = false;
+    return false;
+  },
+};
+
+function set_class(element, name) {
+  if (typeof element.className != 'undefined') {
+    element.className = name;
+  } else {
+    element.setAttribute("class", name);
+  }
+};
+
+function add_listener(event, handler) {
+    if (window.addEventListener)
+      document.addEventListener(event, handler, false);
+    else
+      document.attachEvent("on"+event, handler);
+};
+
+// attach event listeners for initialization
+function slidy_init() { 
+  add_listener("keydown", slidy.key_down);
+  add_listener("keypress", slidy.key_press);
+};
+
+
+