ab2a29f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1658 from david-christiansen/todo-removal

Removal of minor TODOs

commitab2a29f8a7a6285ebb1ffaec5954026dad6595f5 authorEdwin Brady <edwin.brady@gmail.com> dateSat 18 Oct 2014, 22:34 (12 years ago) parentcdff1db 30580db

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

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

10851085unitTy = sUN "Unit"

10861086unitCon = sUN "MkUnit"

10871087

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

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

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

10911090 "\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}",