89a975e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improve ideslave highlighting of primitives

89a975eDavid Raymond Christiansen12 years ago

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

@@ -530,7 +530,7 @@ renderWidth = do iw <- getWidth

530

531

532type1Doc :: Doc OutputAnnotation

533−type1Doc = (annotate AnnConstType $ text "Type 1")

533+type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")

534

535

536isetPrompt :: String -> Idris ()

src/Idris/AbsSyntaxTree.hs+14−17

@@ -1130,10 +1130,12 @@ instance Pretty PTerm OutputAnnotation where

1130-- terminal.

1131consoleDecorate :: IState -> OutputAnnotation -> String -> String

1132consoleDecorate ist _ | not (idris_colourRepl ist) = id

1133−consoleDecorate ist AnnConstData = let theme = idris_colourTheme ist

1133+consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist

1134+ in if constIsType c

1135+ then colouriseType theme

1134− in colouriseData theme

1136+ else colouriseData theme

1135−consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist

1137+consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)

1136− in colouriseType theme

1138+consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)

1137consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)

1139consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)

1138consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)

1140consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)

1139consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

1141consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

@@ -1175,7 +1177,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1175 prettySe p bnd (PPatvar fc n) = pretty n

1177 prettySe p bnd (PPatvar fc n) = pretty n

1176 prettySe p bnd e

1178 prettySe p bnd e

1177 | Just str <- slist p bnd e = str

1179 | Just str <- slist p bnd e = str

1178− | Just n <- snat p e = annotate AnnConstData (text (show n))

1180+ | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))

1179 prettySe p bnd (PRef fc n) = prettyName (ppopt_impl ppo) bnd n

1181 prettySe p bnd (PRef fc n) = prettyName (ppopt_impl ppo) bnd n

1180 prettySe p bnd (PLam n ty sc) =

1182 prettySe p bnd (PLam n ty sc) =

1181 bracket p 2 . group . align . hang 2 $

1183 bracket p 2 . group . align . hang 2 $

@@ -1251,7 +1253,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1251 (left l <+> opName) <$> group (right r)

1253 (left l <+> opName) <$> group (right r)

1252 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1254 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1253 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1255 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1254− f == sUN "Symbol_" = annotate AnnConstType $

1256+ f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $

1255 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1257 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1256 prettySe p bnd (PApp _ f as) = -- Normal prefix applications

1258 prettySe p bnd (PApp _ f as) = -- Normal prefix applications

1257 let args = getExps as

1259 let args = getExps as

@@ -1320,13 +1322,8 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1320 where

1322 where

1321 prettyAs =

1323 prettyAs =

1322 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as

1324 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as

1323− prettySe p bnd PType = annotate AnnConstType $ text "Type"

1325+ prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1324− prettySe p bnd (PConstant c) = annotate (annot c) (text (show c))

1326+ prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1325− where annot (AType _) = AnnConstType

1326− annot StrType = AnnConstType

1327− annot PtrType = AnnConstType

1328− annot VoidType = AnnConstType

1329− annot _ = AnnConstData

1330 -- XXX: add pretty for tactics

1327 -- XXX: add pretty for tactics

1331 prettySe p bnd (PProof ts) =

1328 prettySe p bnd (PProof ts) =

1332 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

1329 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

@@ -1378,16 +1375,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1378 slist' _ _ tm = Nothing

1375 slist' _ _ tm = Nothing

1379

1376

1380 slist p bnd e | Just es <- slist' p bnd e = Just $

1377 slist p bnd e | Just es <- slist' p bnd e = Just $

1381− case es of [] -> annotate AnnConstData $ text "[]"

1378+ case es of [] -> annotate (AnnData "" "") $ text "[]"

1382 [x] -> enclose left right . group $

1379 [x] -> enclose left right . group $

1383 prettySe p bnd x

1380 prettySe p bnd x

1384 xs -> (enclose left right .

1381 xs -> (enclose left right .

1385 align . group . vsep .

1382 align . group . vsep .

1386 punctuate comma .

1383 punctuate comma .

1387 map (prettySe p bnd)) xs

1384 map (prettySe p bnd)) xs

1388− where left = (annotate AnnConstData (text "["))

1385+ where left = (annotate (AnnData "" "") (text "["))

1389− right = (annotate AnnConstData (text "]"))

1386+ right = (annotate (AnnData "" "") (text "]"))

1390− comma = (annotate AnnConstData (text ","))

1387+ comma = (annotate (AnnData "" "") (text ","))

1391 slist _ _ _ = Nothing

1388 slist _ _ _ = Nothing

1392

1389

1393 pairElts :: PTerm -> Maybe [PTerm]

1390 pairElts :: PTerm -> Maybe [PTerm]

src/Idris/Core/TT.hs+20−2

@@ -92,8 +92,9 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St

92 -- ^^ The name, classification, docs overview, and pretty-printed type

93 | AnnBoundName Name Bool

94 -- ^^ The name and whether it is implicit

95− | AnnConstData

95+ | AnnConst Const

96− | AnnConstType

96+ | AnnData String String -- ^ type, doc overview

97+ | AnnType String String -- ^ name, doc overview

97 | AnnKeyword

98 | AnnKeyword

98 | AnnFC FC

99 | AnnFC FC

99 | AnnTextFmt TextFormatting

100 | AnnTextFmt TextFormatting

@@ -524,6 +525,23 @@ instance Pretty Const OutputAnnotation where

524 pretty (B32 w) = text . show $ w

525 pretty (B32 w) = text . show $ w

525 pretty (B64 w) = text . show $ w

526 pretty (B64 w) = text . show $ w

526

527

528+-- | Determines whether the input constant represents a type

529+constIsType :: Const -> Bool

530+constIsType (I _) = False

531+constIsType (BI _) = False

532+constIsType (Fl _) = False

533+constIsType (Ch _) = False

534+constIsType (Str _) = False

535+constIsType (B8 _) = False

536+constIsType (B16 _) = False

537+constIsType (B32 _) = False

538+constIsType (B64 _) = False

539+constIsType (B8V _) = False

540+constIsType (B16V _) = False

541+constIsType (B32V _) = False

542+constIsType (B64V _) = False

543+constIsType _ = True

544+

527data Raw = Var Name

545data Raw = Var Name

528 | RBind Name (Binder Raw) Raw

546 | RBind Name (Binder Raw) Raw

529 | RApp Raw Raw

547 | RApp Raw Raw

src/Idris/IdeSlave.hs+29−3

@@ -12,7 +12,7 @@ import Text.Trifecta.Delta

13import Idris.Core.TT

15−import Control.Applicative

15+import Control.Applicative hiding (Const)

17data SExp = SexpList [SExp]

18 | StringAtom String

@@ -84,6 +84,22 @@ maybeProps [] = []

84maybeProps ((n, Just p):ps) = (SymbolAtom n, toSExp p) : maybeProps ps

85maybeProps ((n, Nothing):ps) = maybeProps ps

87+constTy :: Const -> String

88+constTy (I _) = "Int"

89+constTy (BI _) = "Integer"

90+constTy (Fl _) = "Float"

91+constTy (Ch _) = "Char"

92+constTy (Str _) = "String"

93+constTy (B8 _) = "Bits8"

94+constTy (B16 _) = "Bits16"

95+constTy (B32 _) = "Bits32"

96+constTy (B64 _) = "Bits64"

97+constTy (B8V _) = "Bits8x16"

98+constTy (B16V _) = "Bits16x8"

99+constTy (B32V _) = "Bits32x4"

100+constTy (B64V _) = "Bits64x2"

101+constTy _ = "Type"

102+

87instance SExpable OutputAnnotation where

103instance SExpable OutputAnnotation where

88 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),

104 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),

89 (SymbolAtom "implicit", BoolAtom False)] ++

105 (SymbolAtom "implicit", BoolAtom False)] ++

@@ -92,8 +108,18 @@ instance SExpable OutputAnnotation where

92 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),

108 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),

93 (SymbolAtom "decor", SymbolAtom "bound"),

109 (SymbolAtom "decor", SymbolAtom "bound"),

94 (SymbolAtom "implicit", BoolAtom imp)]

110 (SymbolAtom "implicit", BoolAtom imp)]

95− toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]

111+ toSExp (AnnConst c) = toSExp [(SymbolAtom "decor",

112+ SymbolAtom (if constIsType c then "type" else "data")),

113+ (SymbolAtom "type", StringAtom (constTy c)),

114+ (SymbolAtom "doc-overview", StringAtom "Primitive"),

115+ (SymbolAtom "name", StringAtom (show c))]

116+ toSExp (AnnData ty doc) = toSExp [(SymbolAtom "decor", SymbolAtom "data"),

117+ (SymbolAtom "type", StringAtom ty),

118+ (SymbolAtom "doc-overview", StringAtom doc)]

96− toSExp AnnConstType = toSExp [(SymbolAtom "decor", SymbolAtom "type")]

119+ toSExp (AnnType name doc) = toSExp $ [(SymbolAtom "decor", SymbolAtom "type"),

120+ (SymbolAtom "type", StringAtom "Type"),

121+ (SymbolAtom "doc-overview", StringAtom doc)] ++

122+ if not (null name) then [(SymbolAtom "name", StringAtom name)] else []

97 toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]

123 toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]

98 toSExp (AnnFC (FC f (sl, sc) (el, ec))) = toSExp [(SymbolAtom "source-loc",

124 toSExp (AnnFC (FC f (sl, sc) (el, ec))) = toSExp [(SymbolAtom "source-loc",

99 ((SymbolAtom "filename", StringAtom f),

125 ((SymbolAtom "filename", StringAtom f),

src/Idris/IdrisDoc.hs+7−5

@@ -5,7 +5,7 @@

5module Idris.IdrisDoc (generateDocs) where

7import Idris.Core.TT (Name (..), sUN, SpecialName (..), OutputAnnotation (..),

8− TextFormatting (..), txt, str, nsroot)

8+ TextFormatting (..), txt, str, nsroot, constIsType)

9import Idris.Core.Evaluate (ctxtAlist, Def (..), lookupDefAcc,

10 Accessibility (..), isDConName, isFnName,

11 isTConName)

@@ -455,15 +455,17 @@ genTypeHeader ist (FD n _ args ftype _) = do

455 H.span ! class_ "word" $ do nbsp; ":"; nbsp

456 H.span ! class_ "signature" $ preEscapedToHtml htmlSignature

457

458− where

458+ where

459 htmlSignature = displayDecorated decorator $ renderCompact signature

460 signature = pprintPTerm defaultPPOption [] names (idris_infixes ist) ftype

461 names = [ n | (n@(UN n'), _, _, _) <- args,

462 not (T.isPrefixOf (txt "__") n') ]

463

464− decorator AnnConstData str = htmlSpan str "data" str

464+ decorator (AnnConst c) str | constIsType c = htmlSpan str "type" str

465+ | otherwise = htmlSpan str "data" str

465− decorator AnnConstType str = htmlSpan str "type" str

466+ decorator (AnnData _ _) str = htmlSpan str "data" str

466− decorator AnnKeyword str = htmlSpan "" "keyword" str

467+ decorator (AnnType _ _) str = htmlSpan str "type" str

468+ decorator AnnKeyword str = htmlSpan "" "keyword" str

467 decorator (AnnBoundName n i) str | Just t <- M.lookup n docs =

469 decorator (AnnBoundName n i) str | Just t <- M.lookup n docs =

468 let cs = (if i then "implicit " else "") ++ "documented boundvar"

470 let cs = (if i then "implicit " else "") ++ "documented boundvar"

469 in htmlSpan t cs str

471 in htmlSpan t cs str