git.iko.soy/Idris-dev
on master help sign in
Improve ideslave highlighting of primitives
commit89a975e05eb44374833bf031ab10160f5797fbc8 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 6 May 2014, 13:55 (12 years ago) parent4856076
5 files changed+71−28
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+1−1 src/Idris/AbsSyntaxTree.hs+14−17 src/Idris/Core/TT.hs+20−2 src/Idris/IdeSlave.hs+29−3 src/Idris/IdrisDoc.hs+7−5
src/Idris/AbsSyntax.hs+1−1
@@ -530,7 +530,7 @@ renderWidth = do iw <- getWidth
530530
531531
532532type1Doc :: Doc OutputAnnotation
533−type1Doc = (annotate AnnConstType $ text "Type 1")
533+type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
534534
535535
536536isetPrompt :: String -> Idris ()
src/Idris/AbsSyntaxTree.hs+14−17
@@ -1130,10 +1130,12 @@ instance Pretty PTerm OutputAnnotation where
11301130-- terminal.
11311131consoleDecorate :: IState -> OutputAnnotation -> String -> String
11321132consoleDecorate ist _ | not (idris_colourRepl ist) = id
1133−consoleDecorate ist AnnConstData = let theme = idris_colourTheme ist
1134− in colouriseData theme
1135−consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist
1136− in colouriseType theme
1133+consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1134+ in if constIsType c
1135+ then colouriseType theme
1136+ else colouriseData theme
1137+consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1138+consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
11371139consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
11381140consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
11391141consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
@@ -1175,7 +1177,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
11751177 prettySe p bnd (PPatvar fc n) = pretty n
11761178 prettySe p bnd e
11771179 | 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))
11791181 prettySe p bnd (PRef fc n) = prettyName (ppopt_impl ppo) bnd n
11801182 prettySe p bnd (PLam n ty sc) =
11811183 bracket p 2 . group . align . hang 2 $
@@ -1251,7 +1253,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
12511253 (left l <+> opName) <$> group (right r)
12521254 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
12531255 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1254− f == sUN "Symbol_" = annotate AnnConstType $
1256+ f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
12551257 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
12561258 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
12571259 let args = getExps as
@@ -1320,13 +1322,8 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
13201322 where
13211323 prettyAs =
13221324 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1323− prettySe p bnd PType = annotate AnnConstType $ text "Type"
1324− prettySe p bnd (PConstant c) = annotate (annot c) (text (show c))
1325− where annot (AType _) = AnnConstType
1326− annot StrType = AnnConstType
1327− annot PtrType = AnnConstType
1328− annot VoidType = AnnConstType
1329− annot _ = AnnConstData
1325+ prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1326+ prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
13301327 -- XXX: add pretty for tactics
13311328 prettySe p bnd (PProof ts) =
13321329 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
@@ -1378,16 +1375,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
13781375 slist' _ _ tm = Nothing
13791376
13801377 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 "[]"
13821379 [x] -> enclose left right . group $
13831380 prettySe p bnd x
13841381 xs -> (enclose left right .
13851382 align . group . vsep .
13861383 punctuate comma .
13871384 map (prettySe p bnd)) xs
1388− where left = (annotate AnnConstData (text "["))
1389− right = (annotate AnnConstData (text "]"))
1390− comma = (annotate AnnConstData (text ","))
1385+ where left = (annotate (AnnData "" "") (text "["))
1386+ right = (annotate (AnnData "" "") (text "]"))
1387+ comma = (annotate (AnnData "" "") (text ","))
13911388 slist _ _ _ = Nothing
13921389
13931390 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
9292 -- ^^ The name, classification, docs overview, and pretty-printed type
9393 | AnnBoundName Name Bool
9494 -- ^^ The name and whether it is implicit
95− | AnnConstData
96− | AnnConstType
95+ | AnnConst Const
96+ | AnnData String String -- ^ type, doc overview
97+ | AnnType String String -- ^ name, doc overview
9798 | AnnKeyword
9899 | AnnFC FC
99100 | AnnTextFmt TextFormatting
@@ -524,6 +525,23 @@ instance Pretty Const OutputAnnotation where
524525 pretty (B32 w) = text . show $ w
525526 pretty (B64 w) = text . show $ w
526527
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+
527545data Raw = Var Name
528546 | RBind Name (Binder Raw) Raw
529547 | RApp Raw Raw
src/Idris/IdeSlave.hs+29−3
@@ -12,7 +12,7 @@ import Text.Trifecta.Delta
1212
1313import Idris.Core.TT
1414
15−import Control.Applicative
15+import Control.Applicative hiding (Const)
1616
1717data SExp = SexpList [SExp]
1818 | StringAtom String
@@ -84,6 +84,22 @@ maybeProps [] = []
8484maybeProps ((n, Just p):ps) = (SymbolAtom n, toSExp p) : maybeProps ps
8585maybeProps ((n, Nothing):ps) = maybeProps ps
8686
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+
87103instance SExpable OutputAnnotation where
88104 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),
89105 (SymbolAtom "implicit", BoolAtom False)] ++
@@ -92,8 +108,18 @@ instance SExpable OutputAnnotation where
92108 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),
93109 (SymbolAtom "decor", SymbolAtom "bound"),
94110 (SymbolAtom "implicit", BoolAtom imp)]
95− toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]
96− toSExp AnnConstType = toSExp [(SymbolAtom "decor", SymbolAtom "type")]
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)]
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 []
97123 toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]
98124 toSExp (AnnFC (FC f (sl, sc) (el, ec))) = toSExp [(SymbolAtom "source-loc",
99125 ((SymbolAtom "filename", StringAtom f),
src/Idris/IdrisDoc.hs+7−5
@@ -5,7 +5,7 @@
55module Idris.IdrisDoc (generateDocs) where
66
77import Idris.Core.TT (Name (..), sUN, SpecialName (..), OutputAnnotation (..),
8− TextFormatting (..), txt, str, nsroot)
8+ TextFormatting (..), txt, str, nsroot, constIsType)
99import Idris.Core.Evaluate (ctxtAlist, Def (..), lookupDefAcc,
1010 Accessibility (..), isDConName, isFnName,
1111 isTConName)
@@ -455,15 +455,17 @@ genTypeHeader ist (FD n _ args ftype _) = do
455455 H.span ! class_ "word" $ do nbsp; ":"; nbsp
456456 H.span ! class_ "signature" $ preEscapedToHtml htmlSignature
457457
458− where
458+ where
459459 htmlSignature = displayDecorated decorator $ renderCompact signature
460460 signature = pprintPTerm defaultPPOption [] names (idris_infixes ist) ftype
461461 names = [ n | (n@(UN n'), _, _, _) <- args,
462462 not (T.isPrefixOf (txt "__") n') ]
463463
464− decorator AnnConstData str = htmlSpan str "data" str
465− decorator AnnConstType str = htmlSpan str "type" str
466− decorator AnnKeyword str = htmlSpan "" "keyword" str
464+ decorator (AnnConst c) str | constIsType c = htmlSpan str "type" str
465+ | otherwise = htmlSpan str "data" str
466+ decorator (AnnData _ _) str = htmlSpan str "data" str
467+ decorator (AnnType _ _) str = htmlSpan str "type" str
468+ decorator AnnKeyword str = htmlSpan "" "keyword" str
467469 decorator (AnnBoundName n i) str | Just t <- M.lookup n docs =
468470 let cs = (if i then "implicit " else "") ++ "documented boundvar"
469471 in htmlSpan t cs str