@@ -201,7 +201,9 @@ renderExternal fmt width doc
201 decorate HTMLOutput (AnnName _ _ _ _) = id
201 decorate HTMLOutput (AnnName _ _ _ _) = id
202 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
202 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
203 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
203 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
204− decorate HTMLOutput (AnnConst _) = id -- TODO
204+ decorate HTMLOutput (AnnConst c) =
205+ tag (if constIsType c then "idris-type" else "idris-data")
206+ (Just $ constDocs c)
205 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
207 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
206 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
208 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
207 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
209 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
@@ -222,7 +224,8 @@ renderExternal fmt width doc
222 decorate LaTeXOutput (AnnName _ _ _ _) = id
224 decorate LaTeXOutput (AnnName _ _ _ _) = id
223 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
225 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
224 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
226 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
225− decorate LaTeXOutput (AnnConst _) = id -- TODO
227+ decorate LaTeXOutput (AnnConst c) =
228+ latex $ if constIsType c then "IdrisType" else "IdrisData"
226 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
229 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
227 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
230 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
228 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"
231 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"