diff --git a/AgdaHighlight.hs b/AgdaHighlight.hs new file mode 100644 --- /dev/null +++ b/AgdaHighlight.hs @@ -0,0 +1,120 @@ +{-# 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 @@ -7,11 +7,14 @@ import System.Console.CmdArgs.Implicit import System.FilePath +import Data.Version + ------------------ data Args = Args { sourcedir :: String + , includedir :: [String] , gendir :: String , exercisedir :: String , templatedir :: String @@ -36,6 +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." , 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 +58,7 @@ , 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." - } &= summary "activehs 0.2, (C) 2010-2011 Péter Diviánszky" + } &= summary ("activehs " ++ showVersion version ++ ", (C) 2010-2012 Péter Diviánszky") &= program "activehs" completeArgs :: Args -> IO Args diff --git a/CheckAgdaCode.hs b/CheckAgdaCode.hs new file mode 100644 --- /dev/null +++ b/CheckAgdaCode.hs @@ -0,0 +1,175 @@ +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 @@ -15,10 +15,8 @@ import qualified Language.Haskell.Exts.Pretty as HPty import qualified Language.Haskell.Exts.Syntax as HSyn -{- Agda support (unfinished) import qualified Agda.Syntax.Concrete as ASyn import qualified Agda.Utils.Pretty as AUtil --} import Text.XHtml.Strict hiding (lang) import Text.Pandoc @@ -43,7 +41,7 @@ -- x <- system $ recompilecmd ++ " " ++ input let (ghc:args) = words recompilecmd -- !!! (x, out, err) <- readProcessWithExitCode ghc (args ++ [input]) "" - if x == ExitSuccess + if x == ExitSuccess then do restart ghci return () @@ -65,7 +63,7 @@ extract :: ParseMode -> Bool -> TaskChan -> Args -> Language -> Doc -> IO () extract mode verbose ghci (Args {lang, templatedir, sourcedir, exercisedir, gendir, magicname}) what (Doc meta modu ss) = do - writeEx (what <.> ext) [showEnv $ importsHiding []] + writeEx (what <.> ext) [showEnv mode $ importsHiding []] ss' <- zipWithM processBlock [1..] $ preprocessForSlides ss ht <- readFile' $ templatedir lang' ++ ".template" @@ -103,13 +101,13 @@ when verbose $ putStrLn $ "executing " ++ s system s - importsHiding funnames = case mode of - HaskellMode -> HPty.prettyPrint $ - HSyn.Module loc (HSyn.ModuleName "Main") directives Nothing Nothing - ([mkImport modname funnames, mkImport_ ('X':magicname) modname] ++ imps) [] - AgdaMode -> "" - where - HaskellModule (HSyn.Module loc (HSyn.ModuleName modname) directives _ _ imps _) = modu + importsHiding funnames = case modu of + HaskellModule (HSyn.Module loc (HSyn.ModuleName modname) directives _ _ imps _) -> + 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" mkCodeBlock l = [ CodeBlock ("", ["haskell"], []) $ intercalate "\n" l | not $ null l ] @@ -125,12 +123,12 @@ processBlock _ (Exercise _ visi hidden funnames is) = do let i = show $ mkId $ unlines funnames j = "_j" ++ i - fn = what ++ "_" ++ i <.> "hs" + fn = what ++ "_" ++ i <.> ext (static_, inForm, rows) = if null hidden then ([], visi, length visi) else (visi, [], 2 + length hidden) - writeEx fn [ showEnv $ importsHiding funnames ++ "\n" ++ unlines static_ + writeEx fn [ showEnv mode $ importsHiding funnames ++ "\n" ++ unlines static_ , unlines $ hidden, show $ map parseQuickCheck is, j, i , show funnames ] return @@ -142,10 +140,10 @@ processBlock ii (OneLineExercise p erroneous exp) = do let m5 = mkId $ show ii ++ exp i = show m5 - fn = what ++ (if p == 'R' then "_" ++ i else "") <.> "hs" + fn = what ++ (if p == 'R' then "_" ++ i else "") <.> ext act = getOne "eval" fn i i - when (p == 'R') $ writeEx fn [showEnv $ importsHiding [], "\n" ++ magicname ++ " = " ++ exp] + when (p == 'R') $ writeEx fn [showEnv mode $ importsHiding [], "\n" ++ magicname ++ " = " ++ exp] (b, exp') <- if p == 'F' && all (==' ') exp then return (True, []) else do @@ -240,11 +238,15 @@ ----------------- -showEnv :: String -> String -showEnv prelude +showEnv :: ParseMode -> String -> String +showEnv HaskellMode prelude = "{-# 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 diff --git a/Main.hs b/Main.hs --- a/Main.hs +++ b/Main.hs @@ -44,7 +44,7 @@ main = getArgs >>= mainWithArgs mainWithArgs :: Args -> IO () -mainWithArgs args@(Args {port, static, logdir, hoogledb, fileservedir, gendir, mainpage, restartpath, sourcedir}) = do +mainWithArgs args@(Args {port, static, logdir, hoogledb, fileservedir, gendir, mainpage, restartpath, sourcedir, includedir}) = do ch <- startGHCiServer [sourcedir] (logdir "interpreter") hoogledb cache <- newCache 10 @@ -63,7 +63,7 @@ <|> ifTop (redirect $ fromString mainpage) <|> path (fromString restartpath) (liftIO $ restart ch >> clearCache cache) ) - <|> method POST (exerciseServer (cache, ch) args) + <|> method POST (exerciseServer (sourcedir:includedir) (cache, ch) args) <|> notFound ) where @@ -95,8 +95,8 @@ type TaskChan' = (Cache (Int, T.Text), TaskChan) -exerciseServer :: TaskChan' -> Args -> Snap () -exerciseServer (cache, ch) args@(Args {magicname, lang, exercisedir, verboseinterpreter}) = do +exerciseServer :: [FilePath] -> TaskChan' -> Args -> Snap () +exerciseServer sourcedirs (cache, ch) args@(Args {magicname, lang, exercisedir, verboseinterpreter}) = do params <- fmap show getParams when (length params > 3000) $ do writeText "Too long request." @@ -116,8 +116,9 @@ Just [ss, fn_, x, y, T.unpack -> lang'] <- fmap sequence $ mapM getParam' ["c","f","x","y","lang"] let fn = exercisedir T.unpack fn_ + ext = reverse $ takeWhile (/='.') $ reverse fn True <- liftIO $ doesFileExist fn - Just task <- liftIO $ fmap (eval_ ss y . T.splitOn (T.pack delim)) $ T.readFile fn + Just task <- liftIO $ fmap (eval_ ext ss y . T.splitOn (T.pack delim)) $ T.readFile fn liftIO $ exerciseServer' ('X':magicname) ch verboseinterpreter fn x lang md5Id task <|> return [Error True $ translate lang "Inconsistency between server and client."] @@ -130,17 +131,17 @@ return res where - eval_ "eval" _ [_] + eval_ _ "eval" _ [_] = Just Eval - eval_ "eval" _ [_, goodsol] + eval_ _ "eval" _ [_, goodsol] = Just $ Compare magicname $ T.unpack $ T.drop (length magicname + 4) $ goodsol - eval_ comm + eval_ ext comm (T.unpack -> s) [env, hidden, re -> Just (is :: [([String],String)]), T.unpack -> j, T.unpack -> i, re -> Just funnames] = Just $ case comm of "eval2" -> Compare2 env funnames s - "check" -> Check env funnames is i j - eval_ _ _ _ + "check" -> Check ext sourcedirs env funnames is i j + eval_ _ _ _ _ = Nothing maybeRead :: Read a => String -> Maybe a diff --git a/Parse.hs b/Parse.hs --- a/Parse.hs +++ b/Parse.hs @@ -79,10 +79,10 @@ case readMarkdown pState . unlines . concatMap preprocess . lines $ c of Pandoc meta (CodeBlock ("",["sourceCode","literate","haskell"],[]) h: blocks) -> do header <- parseModule mode $ h - fmap (Doc meta header) $ collectTests mode $ map (highlight . interpreter . Text) blocks + fmap (Doc meta header) $ collectTests mode $ map ({-highlight . -}interpreter . Text) blocks Pandoc meta blocks -> do header <- parseModule mode $ "module Unknown where" - fmap (Doc meta header) $ collectTests mode $ map (highlight . interpreter . Text) blocks + 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) @@ -95,7 +95,7 @@ preprocess ('|':l) = [] -- drop lines ending with "--" - preprocess l | drop ((length l) - 2) l == "--" = [] + preprocess l | take 3 (dropWhile (==' ') $ reverse l) == "-- " = [] | otherwise = [l] pState = defaultParserState @@ -141,32 +141,32 @@ {- Agda support (unfinished) -} processAgdaLines :: Bool -> String -> IO ([String], [String], [Name]) processAgdaLines isExercise l_ = do - return ([], [], []) -{- +-- return ([], [], []) + let l = parts l_ - x <- fmap (zip l) $ mapM (Agda.parse Agda.moduleParser . ("module X where\n"++) . unlines) 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 [Agda.Module _ _ _ [Agda.TypeSig _ n _]] + getFName [ASyn.Module _ _ _ [ASyn.TypeSig _ n _]] = [n] getFName _ = [] -- isVisible [Agda.Module _ _ [Agda.TypedBindings _ (Agda.Arg _ _ [Agda.TBind _ a _])] declarations] -- = True - isVisible [Agda.Module _ _ _ [Agda.TypeSig _ n _]] = True + isVisible [ASyn.Module _ _ _ [ASyn.TypeSig _ n _]] = True isVisible _ = not isExercise (visible, hidden) = partition (isVisible . snd . snd) x - toName n = Ident $ show n + 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/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,2 +1,3 @@ import Distribution.Simple + main = defaultMain diff --git a/Special.hs b/Special.hs --- a/Special.hs +++ b/Special.hs @@ -6,6 +6,7 @@ import Smart import QuickCheck +import CheckAgdaCode import Result import Lang import Html @@ -48,7 +49,7 @@ = Eval | Compare String String | Compare2 T.Text [String] String - | Check T.Text [String] [([String],String)] String String + | Check String [FilePath] T.Text [String] [([String],String)] String String exerciseServer' :: String @@ -86,23 +87,30 @@ return $ compareMistGen lang (show m5) x $ goodsol eval (Compare2 env funnames s) = do - fn' <- tmpSaveHs (show m5) $ env `T.append` sol + fn' <- tmpSaveHs "hs" (show m5) $ env `T.append` sol case qualify qualifier funnames s of Left err -> return [Error True err] Right s2 -> interp verbose m5 lang ch fn' s $ \a -> fmap (compareClearGen lang (show m5)) $ interpret (wrap2 a s2) (as :: WrapData2) - eval (Check env funnames is i j) = do - fn' <- tmpSaveHs (show m5) $ env `T.append` sol - 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] + eval (Check ext sourcedirs env funnames is i j) = do + fn' <- tmpSaveHs ext (show m5) $ env `T.append` sol + case ext of + "hs" -> do + 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 -> T.Text -> IO FilePath -tmpSaveHs x s = do +tmpSaveHs :: String -> String -> T.Text -> IO FilePath +tmpSaveHs ext x s = do tmpdir <- getTemporaryDirectory - let tmp = tmpdir "GHCiServer_" ++ x ++ ".hs" - T.writeFile tmp s + let name = "GHCiServer_" ++ x + 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 +version: 0.3.0.1 category: Education, Documentation synopsis: Haskell code presentation tool description: @@ -50,41 +50,43 @@ HoogleCustom, Html, QuickCheck, + CheckAgdaCode, + AgdaHighlight, Special Build-Depends: - Agda, - highlighting-kate, - hoogle >= 4.2 && < 4.3, + 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, dia-functions >= 0.2.1.1 && < 0.3, activehs-base >= 0.2 && < 0.4, data-pprint >= 0.2 && < 0.3, - base >= 4.0 && < 4.6, - QuickCheck >= 2.4 && < 2.5, + base >= 4.0 && < 4.7, + QuickCheck >= 2.4 && < 2.6, array >= 0.3 && < 0.5, - directory >= 1.1 && < 1.2, - containers >= 0.4 && < 0.5, + directory >= 1.1 && < 1.3, + containers >= 0.4 && < 0.6, filepath >= 1.2 && < 1.4, text >= 0.11 && < 0.12, - snap-core >= 0.6 && < 0.8, - snap-server >= 0.6 && < 0.8, + snap-core >= 0.6 && < 0.10, + snap-server >= 0.6 && < 0.10, syb >= 0.2 && < 0.4, - haskell-src-exts >= 1.9 && < 1.12, - bytestring >= 0.9 && < 0.10, + haskell-src-exts >= 1.12 && < 1.14, + bytestring >= 0.9 && < 0.11, utf8-string >= 0.3 && < 0.4, xhtml >= 3000.2 && < 3000.3, - blaze-html >= 0.4 && < 0.5, + blaze-html >= 0.4 && < 0.6, pureMD5 >= 2.1 && < 2.2, deepseq >= 1.1 && < 1.4, - split >= 0.1 && < 0.2, + split >= 0.1 && < 0.3, pandoc >= 1.8 && < 1.10, 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, - mtl >= 2.0 && < 2.1, + mtl >= 2.0 && < 2.2, old-locale >= 1.0 && < 1.1, - cmdargs >= 0.7 && < 0.10 + cmdargs >= 0.7 && < 0.11