ab2a29f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

ab2a29fEdwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs−1

compare with master

unifiedsplit

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

1085unitTy = sUN "Unit"

1086unitCon = sUN "MkUnit"

1087

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

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

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

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

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

1091 "\n\n" ++

1090 "\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

173 when (ErrorHandler `elem` opts) $ do

174 if errorReflection

175 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:

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

178 if tyIsHandler nty'

179 then do i <- getIState

src/Idris/Output.hs+13−3

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

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

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

220 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++">"

222 decorate HTMLOutput (AnnTerm _ _) = id

227 decorate HTMLOutput (AnnTerm _ _) = id

223 decorate HTMLOutput (AnnSearchResult _) = id

228 decorate HTMLOutput (AnnSearchResult _) = id

224 decorate HTMLOutput (AnnErr _) = id

229 decorate HTMLOutput (AnnErr _) = id

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

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

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

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

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

243 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"

248 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"

245 decorate LaTeXOutput (AnnTerm _ _) = id

254 decorate LaTeXOutput (AnnTerm _ _) = id

246 decorate LaTeXOutput (AnnSearchResult _) = id

255 decorate LaTeXOutput (AnnSearchResult _) = id

247 decorate LaTeXOutput (AnnErr _) = id

256 decorate LaTeXOutput (AnnErr _) = id

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

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

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

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

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

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

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

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

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

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

264 wrap LaTeXOutput str =

274 wrap LaTeXOutput str =

265 concat . intersperse "\n" $

275 concat . intersperse "\n" $

266 ["\\documentclass{article}",

276 ["\\documentclass{article}",