> module Idris.Fontlock(htmlise,latexise) where
> import Data.Char
> import List
> import Idris.AbsSyntax
> import Idris.Lexer
> import Idris.Context
> data Markup = DC | TC | FN | CM | VV | KW | ST | CH | LCM
> | BRK | SEC | SUBSEC
> | TITLE | AUTHOR | HTML | LATEX | None
> deriving Show
> hclass DC = "datacon"
> hclass TC = "typecon"
> hclass FN = "function"
> hclass CM = "comment"
> hclass VV = "variable"
> hclass KW = "keyword"
> hclass ST = "string"
> hclass CH = "string"
> hclass _ = ""
> mkMarkups :: Ctxt IvorFun -> [(String, Markup)]
> mkMarkups ctxt = map mkMarkup (map (\ (x,y) -> (x, rawDecl y)) (ctxtAlist ctxt))
> mkMarkup :: (Id, Decl) -> (String, Markup)
> mkMarkup (n, Fun _ _) = (show n, FN)
> mkMarkup (n, Fwd _ _ _) = (show n, FN)
> mkMarkup (n, TermDef _ _ _) = (show n, FN)
> mkMarkup (n, Prf _) = (show n, FN)
> mkMarkup (n, DataDecl _) = (show n, TC)
> mkMarkup (n, Constructor) = (show n, DC)
> mkMarkup (n, _) = (show n, VV)
> getMarkup :: String -> [(String, Markup)] -> Markup
> getMarkup x ms = case lookup x ms of
> Just m -> m
> Nothing -> VV
> markupText :: [(String, Markup)] -> String -> [(Markup, String)]
> markupText ms ('-':'-':' ':'I':'G':'N':'O':'R':'E':xs) = endIgnore ms xs
> markupText ms ('-':'-':'\n':xs) = (BRK, ""):markupText ms xs
> markupText ms ('-':'-':' ':'S':'e':'c':'t':'i':'o':'n':':':' ':xs)
> = markupSECtoNewline SEC "" ms xs
> markupText ms ('-':'-':' ':'T':'i':'t':'l':'e':':':' ':xs)
> = markupSECtoNewline TITLE "" ms xs
> markupText ms ('-':'-':' ':'L':'a':'T':'e':'X':':':' ':xs)
> = markupSECtoNewline LATEX "" ms xs
> markupText ms ('-':'-':' ':'H':'T':'M':'L':':':' ':xs)
> = markupSECtoNewline HTML "" ms xs
> markupText ms ('-':'-':' ':'A':'u':'t':'h':'o':'r':':':' ':xs)
> = markupSECtoNewline AUTHOR "" ms xs
> markupText ms ('-':'-':' ':'S':'u':'b':'s':'e':'c':'t':'i':'o':'n':':':' ':xs)
> = markupSECtoNewline SUBSEC "" ms xs
> markupText ms ('-':'-':xs) = markupCMtoNewline "" ms xs
> markupText ms ('{':'-':'>':xs) = markupText ms xs
> markupText ms ('>':'-':'}':xs) = markupText ms xs
> markupText ms ('{':'-':'-':xs) = markupLCM "" ms xs
> markupText ms ('{':'-':xs) = markupCM "" ms xs
> markupText ms ('\'':c:'\'':xs) = (CH, ['\'',c,'\'']):markupText ms xs
> markupText ms ('"':xs) = markupString ms xs
> markupText ms ('%':xs) = markupSpecial ms xs
> markupText ms ('\t':xs) = (None, " "):markupText ms xs
> markupText ms (c:cs)
> | isAlpha c || c=='_' = markupVar ms (c:cs)
> markupText ms (c:cs) = (None, [c]):markupText ms cs
> markupText ms [] = []
> keywords = ["proof","data","using","idiom","params","namespace","module",
> "import","export","inline","where","partial","syntax","lazy",
> "infix","infixl","infixr","do","refl","if","then","else","let",
> "in","return","include","exists", "with"]
> types = ["String","Int","Char","Float","Ptr","Lock","Handle","Set"]
> markupSpecial ms cs = case span isAllowed cs of
> (var,rest) -> (None, '%':var):(markupText ms rest)
> markupVar ms cs = case span isAllowed cs of
> (var,rest) -> if (var `elem` keywords)
> then (KW, var):(markupText ms rest)
> else if (var `elem` types)
> then (TC, var):(markupText ms rest)
> else (getMarkup var ms, var):(markupText ms rest)
> markupCMtoNewline acc ms ('\n':xs) = (CM, "--"++reverse acc):
> markupText ms ('\n':xs)
> markupCMtoNewline acc ms (x:xs) = markupCMtoNewline (x:acc) ms xs
> markupCMtoNewline acc ms [] = (CM, "--"++reverse acc):[]
> markupSECtoNewline sec acc ms ('\n':xs) = (sec, reverse acc):
> markupText ms ('\n':xs)
> markupSECtoNewline sec acc ms (x:xs) = markupSECtoNewline sec (x:acc) ms xs
> markupSECtoNewline sec acc ms [] = (sec, reverse acc):[]
> markupCM acc ms ('-':'}':xs) = (CM, "{-"++reverse acc++"-}"):markupText ms xs
> markupCM acc ms (x:xs) = markupCM (x:acc) ms xs
> markupCM acc ms [] = (CM, "{-"++reverse acc):[]
> markupLCM acc ms ('-':'-':'}':xs) = (LCM, reverse acc):markupText ms xs
> markupLCM acc ms (x:xs) = markupLCM (x:acc) ms xs
> markupLCM acc ms [] = (LCM, reverse acc):[]
> endIgnore ms ('-':'-':' ':'S':'T':'A':'R':'T':'\n':xs) = markupText ms xs
> endIgnore ms (x:xs) = endIgnore ms xs
> endIgnore ms [] = []
> markupString ms xs = case getstr xs of
> Just (str, rest, nls) -> (ST, show str):markupText ms rest
> htmlise :: Ctxt IvorFun -> FilePath -> FilePath -> Maybe FilePath -> IO ()
> htmlise ctxt fp outf style
> = do txt <- readFile fp
> let ms = mkMarkups ctxt
> let mtxt = markupText ms txt
> writeFile outf (renderHTML fp style mtxt)
> latexise :: Ctxt IvorFun -> FilePath -> FilePath -> IO ()
> latexise ctxt fp outf = do txt <- readFile fp
> let ms = mkMarkups ctxt
> let mtxt = markupText ms txt
> writeFile outf (renderLatex mtxt)
> skipnl :: [(Markup, String)] -> [(Markup, String)]
> skipnl ((None, "\n"):xs) = skipnl xs
> skipnl xs = xs
> skipIfBrk :: [(Markup, String)] -> [(Markup, String)]
> skipIfBrk xs = si xs xs
> where si orig next@((BRK, _):xs) = next
> si orig next@((TITLE, _):xs) = next
> si orig next@((HTML, _):xs) = next
> si orig next@((LATEX, _):xs) = next
> si orig next@((AUTHOR, _):xs) = next
> si orig next@((SEC, _):xs) = next
> si orig next@((SUBSEC, _):xs) = next
> si orig next@((LCM, _):xs) = next
> si orig ((None, "\n"):xs) = si orig xs
> si orig _ = orig
> renderHTML :: String -> Maybe String -> [(Markup, String)] -> String
> renderHTML title style ms = htmlHeader title style ++
> "\n" ++ html (skipIfBrk ms) ++ "\n
\n\n