agda-server-0.1: JSDictDef.hs

--   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