activehs 0.3 → 0.3.0.1
raw patch · 9 files changed
+378/−65 lines, 9 filesdep ~Agdadep ~QuickCheckdep ~basesetup-changed
Dependency ranges changed: Agda, QuickCheck, base, blaze-html, bytestring, cmdargs, containers, directory, haskell-src-exts, highlighting-kate, hoogle, mtl, snap-core, snap-server, split
Files
- AgdaHighlight.hs +120/−0
- Args.hs +5/−1
- CheckAgdaCode.hs +175/−0
- Converter.hs +19/−17
- Main.hs +11/−10
- Parse.hs +10/−10
- Setup.hs +1/−0
- Special.hs +19/−11
- activehs.cabal +18/−16
+ AgdaHighlight.hs view
@@ -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 + })
Args.hs view
@@ -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
+ CheckAgdaCode.hs view
@@ -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+-}+++
Converter.hs view
@@ -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
Main.hs view
@@ -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 "<html xmlns=\"http://www.w3.org/1999/xhtml\"><body>Too long request.</body></html>"@@ -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
Parse.hs view
@@ -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)
Setup.hs view
@@ -1,2 +1,3 @@ import Distribution.Simple+ main = defaultMain
Special.hs view
@@ -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
activehs.cabal view
@@ -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