30580db · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Removal of minor TODOs

Some were completed before and we forgot to remove the TODO, while others I just took care of.

commit30580dbe74c8e351cb347c61814e0bd7df7b54f3 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 18 Oct 2014, 11:31 (12 years ago) parentb0e1ecf

3 files changed+14−5

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs−1 src/Idris/Elab/Type.hs+1−1 src/Idris/Output.hs+13−3

src/Idris/AbsSyntaxTree.hs−1

@@ -1078,7 +1078,6 @@ primNames = [eqTy, eqCon, inferTy, inferCon]

10781078unitTy = sUN "Unit"

10791079unitCon = sUN "MkUnit"

10801080

1081−-- TODO: elaborate the code samples in the docstring

10821081falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $

10831082 "The empty type, also known as the trivially false proposition." ++

10841083 "\n\n" ++

src/Idris/Elab/Type.hs+1−1

@@ -173,7 +173,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

173173 when (ErrorHandler `elem` opts) $ do

174174 if errorReflection

175175 then

176− -- TODO: Check that the declared type is the correct type for an error handler:

176+ -- Check that the declared type is the correct type for an error handler:

177177 -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt

178178 if tyIsHandler nty'

179179 then do i <- getIState

src/Idris/Output.hs+13−3

@@ -218,7 +218,12 @@ renderExternal fmt width doc

218218 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing

219219 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing

220220 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing

221− decorate HTMLOutput (AnnTextFmt _) = id -- TODO

221+ decorate HTMLOutput (AnnTextFmt fmt) =

222+ case fmt of

223+ BoldText -> mkTag "strong"

224+ ItalicText -> mkTag "em"

225+ UnderlineText -> tag "idris-underlined" Nothing

226+ where mkTag t x = "<"++t++">"++x++"</"++t++">"

222227 decorate HTMLOutput (AnnTerm _ _) = id

223228 decorate HTMLOutput (AnnSearchResult _) = id

224229 decorate HTMLOutput (AnnErr _) = id

@@ -241,7 +246,11 @@ renderExternal fmt width doc

241246 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"

242247 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"

243248 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"

244− decorate LaTeXOutput (AnnTextFmt _) = id -- TODO

249+ decorate LaTeXOutput (AnnTextFmt fmt) =

250+ case fmt of

251+ BoldText -> latex "textbf"

252+ ItalicText -> latex "emph"

253+ UnderlineText -> latex "underline"

245254 decorate LaTeXOutput (AnnTerm _ _) = id

246255 decorate LaTeXOutput (AnnSearchResult _) = id

247256 decorate LaTeXOutput (AnnErr _) = id

@@ -260,7 +269,8 @@ renderExternal fmt width doc

260269 ".idris-function {color: green; }",

261270 ".idris-keyword { font-weight: bold; }",

262271 ".idris-bound { color: purple; }",

263− ".idris-implicit { font-style: italic; }"]

272+ ".idris-implicit { font-style: italic; }",

273+ ".idris-underlined { text-decoration: underline; }"]

264274 wrap LaTeXOutput str =

265275 concat . intersperse "\n" $

266276 ["\\documentclass{article}",