15aebc9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add highlighting for keywords in interpreter output

15aebc9David Raymond Christiansen13 years ago

src/Idris/AbsSyntaxTree.hs+10−7

compare with master

unifiedsplit

@@ -1067,6 +1067,7 @@ consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist

1067 in colouriseType theme

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

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

1070+consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

1070consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist

1071consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist

1071 theme = idris_colourTheme ist

1072 theme = idris_colourTheme ist

1072 in case () of

1073 in case () of

@@ -1103,8 +1104,8 @@ pprintPTerm impl bnd = prettySe 10 bnd

1103 prettySe 10 ((n, False):bnd) sc

1104 prettySe 10 ((n, False):bnd) sc

1104 prettySe p bnd (PLet n ty v sc) =

1105 prettySe p bnd (PLet n ty v sc) =

1105 bracket p 2 $

1106 bracket p 2 $

1106− text "let" <+> bindingOf n False <+> text "=" </>

1107+ kwd "let" <+> bindingOf n False <+> text "=" </>

1107− prettySe 10 bnd v <+> text "in" </>

1108+ prettySe 10 bnd v <+> kwd "in" </>

1108 prettySe 10 ((n, False):bnd) sc

1109 prettySe 10 ((n, False):bnd) sc

1109 prettySe p bnd (PPi (Exp l s _) n ty sc)

1110 prettySe p bnd (PPi (Exp l s _) n ty sc)

1110 | n `elem` allNamesIn sc || impl =

1111 | n `elem` allNamesIn sc || impl =

@@ -1137,7 +1138,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

1137 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc

1138 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc

1138 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =

1139 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =

1139 bracket p 2 $

1140 bracket p 2 $

1140− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1141+ lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1141 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1142 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1142 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1143 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1143 | UN nm <- basename f

1144 | UN nm <- basename f

@@ -1177,7 +1178,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

1177 then fp

1178 then fp

1178 else fp <+> align (vsep (map (prettyArgSe bnd) args))

1179 else fp <+> align (vsep (map (prettyArgSe bnd) args))

1179 prettySe p bnd (PCase _ scr opts) =

1180 prettySe p bnd (PCase _ scr opts) =

1180− text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody

1181+ kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody

1181 where

1182 where

1182 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts

1183 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts

1183

1184

@@ -1244,8 +1245,8 @@ pprintPTerm impl bnd = prettySe 10 bnd

1244 prettySe p bnd (PTactics ts) =

1245 prettySe p bnd (PTactics ts) =

1245 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

1246 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

1246 prettySe p bnd (PMetavar n) = text "?" <> pretty n

1247 prettySe p bnd (PMetavar n) = text "?" <> pretty n

1247− prettySe p bnd (PReturn f) = text "return"

1248+ prettySe p bnd (PReturn f) = kwd "return"

1248− prettySe p bnd PImpossible = text "impossible"

1249+ prettySe p bnd PImpossible = kwd "impossible"

1249 prettySe p bnd Placeholder = text "_"

1250 prettySe p bnd Placeholder = text "_"

1250 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"

1251 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"

1251 prettySe p bnd (PElabError s) = pretty s

1252 prettySe p bnd (PElabError s) = pretty s

@@ -1260,7 +1261,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

1260 prettyArgSe bnd arg = prettySe 0 bnd arg

1261 prettyArgSe bnd arg = prettySe 0 bnd arg

1261 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1262 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1262 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace

1263 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace

1263− prettyArgSti bnd (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1264+ prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1264

1265

1265 basename :: Name -> Name

1266 basename :: Name -> Name

1266 basename (NS n _) = basename n

1267 basename (NS n _) = basename n

@@ -1313,6 +1314,8 @@ pprintPTerm impl bnd = prettySe 10 bnd

1313 | inner > outer = lparen <> doc <> rparen

1314 | inner > outer = lparen <> doc <> rparen

1314 | otherwise = doc

1315 | otherwise = doc

1315

1316

1317+ kwd = annotate AnnKeyword . text

1318+

1316-- | Pretty-printer helper for the binding site of a name

1319-- | Pretty-printer helper for the binding site of a name

1317bindingOf :: Name -- ^^ the bound name

1320bindingOf :: Name -- ^^ the bound name

1318 -> Bool -- ^^ whether the name is implicit

1321 -> Bool -- ^^ whether the name is implicit

src/Idris/Colours.hs+4−2

@@ -3,7 +3,7 @@ module Idris.Colours (

3 ColourTheme(..),

4 defaultTheme,

5 colouriseKwd, colouriseBound, colouriseImplicit,

6− colouriseType, colouriseFun, colouriseData,

6+ colouriseType, colouriseFun, colouriseData, colouriseKeyword,

7 colourisePrompt,

8 ColourType(..)) where

@@ -31,7 +31,7 @@ data ColourTheme = ColourTheme { keywordColour :: IdrisColour

31 deriving (Eq, Show)

33defaultTheme :: ColourTheme

34−defaultTheme = ColourTheme { keywordColour = IdrisColour Nothing True True True False

34+defaultTheme = ColourTheme { keywordColour = IdrisColour Nothing True False True False

35 , boundVarColour = mkColour Magenta

36 , implicitColour = IdrisColour (Just Magenta) True True False False

37 , functionColour = mkColour Green

@@ -71,6 +71,8 @@ colouriseData t = colourise (dataColour t)

71colourisePrompt :: ColourTheme -> String -> String

72colourisePrompt t = colourise (promptColour t)

74+colouriseKeyword :: ColourTheme -> String -> String

75+colouriseKeyword t = colourise (keywordColour t)

75data ColourType = KeywordColour

77data ColourType = KeywordColour

76 | BoundVarColour

78 | BoundVarColour

src/Idris/Core/TT.hs+1

@@ -89,6 +89,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)

89 | AnnBoundName Name Bool

90 | AnnConstData

91 | AnnConstType

92+ | AnnKeyword

92 | AnnFC FC

93 | AnnFC FC

94-- | Used for error reflection

95-- | Used for error reflection

src/Idris/IdeSlave.hs+1

@@ -89,6 +89,7 @@ instance SExpable OutputAnnotation where

89 (SymbolAtom "implicit", BoolAtom imp)]

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

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

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

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

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

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

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

94 (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),

95 (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),