on master help sign in
Preserve manual name type annotations
840f588David Raymond Christiansen
src/Idris/Delaborate.hs+8−7
@@ -19,6 +19,7 @@ import Data.Generics.Uniplate.Data (transform)
19import Data.Maybe (mapMaybe)
19import Data.Maybe (mapMaybe)
20import Data.List (intersperse, nub)
20import Data.List (intersperse, nub)
21import qualified Data.Text as T
21import qualified Data.Text as T
22+import Control.Applicative (Alternative((<|>)))
22import Control.Monad.State
23import Control.Monad.State
23
24
24import Debug.Trace
25import Debug.Trace
@@ -566,18 +567,18 @@ annTm tm = annotate (AnnTerm [] tm)
566
567
567-- | Add extra metadata to an output annotation, optionally marking metavariables.
568-- | Add extra metadata to an output annotation, optionally marking metavariables.
568fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation
569fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation
569−fancifyAnnots ist meta annot@(AnnName n _ _ _) =
570+fancifyAnnots ist meta annot@(AnnName n nt _ _) =
570 do let ctxt = tt_ctxt ist
571 do let ctxt = tt_ctxt ist
571 docs = docOverview ist n
572 docs = docOverview ist n
572 ty = Just (getTy ist n)
573 ty = Just (getTy ist n)
573 case () of
574 case () of
574− _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty
575+ _ | isDConName n ctxt -> AnnName n (nt <|> Just DataOutput) docs ty
575− _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty
576+ _ | isFnName n ctxt -> AnnName n (nt <|> Just FunOutput) docs ty
576− _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty
577+ _ | isTConName n ctxt -> AnnName n (nt <|> Just TypeOutput) docs ty
577 _ | isMetavarName n ist -> if meta
578 _ | isMetavarName n ist -> if meta
578− then AnnName n (Just MetavarOutput) docs ty
579+ then AnnName n (nt <|> Just MetavarOutput) docs ty
579− else AnnName n (Just FunOutput) docs ty
580+ else AnnName n (nt <|> Just FunOutput) docs ty
580− _ | isPostulateName n ist -> AnnName n (Just PostulateOutput) docs ty
581+ _ | isPostulateName n ist -> AnnName n (nt <|> Just PostulateOutput) docs ty
581 _ | otherwise -> annot
582 _ | otherwise -> annot
582 where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs
583 where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs
583 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)
584 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)