agda-server (empty) → 0.1
raw patch · 20 files changed
+1649/−0 lines, 20 filesdep +Agdadep +HJavaScriptdep +basesetup-changedbinary-added
Dependencies added: Agda, HJavaScript, base, cmdargs, containers, directory, filepath, mtl, pandoc, snap-core, snap-server, transformers, utf8-string, xhtml
Files
- AgdaInterface.hs +47/−0
- Args.hs +60/−0
- Html.hs +156/−0
- JS.hs +76/−0
- JSDict.hs +202/−0
- JSDictDef.hs +100/−0
- LICENSE +31/−0
- Main.hs +87/−0
- Memo.hs +257/−0
- Param.hs +23/−0
- Setup.hs +2/−0
- Standalone.hs +48/−0
- agda-server.cabal +54/−0
- copy/Agda.css +31/−0
- copy/agda.template +22/−0
- copy/common.css +205/−0
- copy/common.js +6/−0
- copy/common_en.js +81/−0
- copy/icon.ico binary
- copy/slidy.js +161/−0
+ AgdaInterface.hs view
@@ -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+
+ Args.hs view
@@ -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+++
+ Html.hs view
@@ -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++
+ JS.hs view
@@ -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]++
+ JSDict.hs view
@@ -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+++
+ JSDictDef.hs view
@@ -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+
+ LICENSE view
@@ -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.+
+ Main.hs view
@@ -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+++
+ Memo.hs view
@@ -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++
+ Param.hs view
@@ -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++
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Standalone.hs view
@@ -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+ }++
+ agda-server.cabal view
@@ -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+
+ copy/Agda.css view
@@ -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 }
+ copy/agda.template view
@@ -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>+
+ copy/common.css view
@@ -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; */ }+
+ copy/common.js view
@@ -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;});}
+ copy/common_en.js view
@@ -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(); + }+ }+}++
+ copy/icon.ico view
binary file changed (absent → 1150 bytes)
+ copy/slidy.js view
@@ -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);+};+++