git.iko.soy/Idris-dev
on master help sign in
Merge pull request #985 from david-christiansen/keyword-highlight

Add highlighting for keywords in interpreter output

commit1b81d69ecfa1dfeeb3fc1c8f2ba8203c3b41c610 authorEdwin Brady <edwin.brady@gmail.com> dateThu 20 Mar 2014, 11:41 (13 years ago) parent99ab46715aebc9
4 files changed+16−9
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+10−7 src/Idris/Colours.hs+4−2 src/Idris/Core/TT.hs+1 src/Idris/IdeSlave.hs+1
src/Idris/AbsSyntaxTree.hs+10−7
@@ -1067,6 +1067,7 @@ consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist
10671067 in colouriseType theme
10681068consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
10691069consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1070+consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
10701071consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist
10711072 theme = idris_colourTheme ist
10721073 in case () of
@@ -1103,8 +1104,8 @@ pprintPTerm impl bnd = prettySe 10 bnd
11031104 prettySe 10 ((n, False):bnd) sc
11041105 prettySe p bnd (PLet n ty v sc) =
11051106 bracket p 2 $
1106− text "let" <+> bindingOf n False <+> text "=" </>
1107− prettySe 10 bnd v <+> text "in" </>
1107+ kwd "let" <+> bindingOf n False <+> text "=" </>
1108+ prettySe 10 bnd v <+> kwd "in" </>
11081109 prettySe 10 ((n, False):bnd) sc
11091110 prettySe p bnd (PPi (Exp l s _) n ty sc)
11101111 | n `elem` allNamesIn sc || impl =
@@ -1137,7 +1138,7 @@ pprintPTerm impl bnd = prettySe 10 bnd
11371138 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
11381139 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
11391140 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 <>
11411142 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
11421143 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
11431144 | UN nm <- basename f
@@ -1177,7 +1178,7 @@ pprintPTerm impl bnd = prettySe 10 bnd
11771178 then fp
11781179 else fp <+> align (vsep (map (prettyArgSe bnd) args))
11791180 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
11811182 where
11821183 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
11831184
@@ -1244,8 +1245,8 @@ pprintPTerm impl bnd = prettySe 10 bnd
12441245 prettySe p bnd (PTactics ts) =
12451246 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
12461247 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1247− prettySe p bnd (PReturn f) = text "return"
1248− prettySe p bnd PImpossible = text "impossible"
1248+ prettySe p bnd (PReturn f) = kwd "return"
1249+ prettySe p bnd PImpossible = kwd "impossible"
12491250 prettySe p bnd Placeholder = text "_"
12501251 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
12511252 prettySe p bnd (PElabError s) = pretty s
@@ -1260,7 +1261,7 @@ pprintPTerm impl bnd = prettySe 10 bnd
12601261 prettyArgSe bnd arg = prettySe 0 bnd arg
12611262 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
12621263 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
12641265
12651266 basename :: Name -> Name
12661267 basename (NS n _) = basename n
@@ -1313,6 +1314,8 @@ pprintPTerm impl bnd = prettySe 10 bnd
13131314 | inner > outer = lparen <> doc <> rparen
13141315 | otherwise = doc
13151316
1317+ kwd = annotate AnnKeyword . text
1318+
13161319-- | Pretty-printer helper for the binding site of a name
13171320bindingOf :: Name -- ^^ the bound name
13181321 -> Bool -- ^^ whether the name is implicit
src/Idris/Colours.hs+4−2
@@ -3,7 +3,7 @@ module Idris.Colours (
33 ColourTheme(..),
44 defaultTheme,
55 colouriseKwd, colouriseBound, colouriseImplicit,
6− colouriseType, colouriseFun, colouriseData,
6+ colouriseType, colouriseFun, colouriseData, colouriseKeyword,
77 colourisePrompt,
88 ColourType(..)) where
99
@@ -31,7 +31,7 @@ data ColourTheme = ColourTheme { keywordColour :: IdrisColour
3131 deriving (Eq, Show)
3232
3333defaultTheme :: ColourTheme
34−defaultTheme = ColourTheme { keywordColour = IdrisColour Nothing True True True False
34+defaultTheme = ColourTheme { keywordColour = IdrisColour Nothing True False True False
3535 , boundVarColour = mkColour Magenta
3636 , implicitColour = IdrisColour (Just Magenta) True True False False
3737 , functionColour = mkColour Green
@@ -71,6 +71,8 @@ colouriseData t = colourise (dataColour t)
7171colourisePrompt :: ColourTheme -> String -> String
7272colourisePrompt t = colourise (promptColour t)
7373
74+colouriseKeyword :: ColourTheme -> String -> String
75+colouriseKeyword t = colourise (keywordColour t)
7476
7577data ColourType = KeywordColour
7678 | BoundVarColour
src/Idris/Core/TT.hs+1
@@ -89,6 +89,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)
8989 | AnnBoundName Name Bool
9090 | AnnConstData
9191 | AnnConstType
92+ | AnnKeyword
9293 | AnnFC FC
9394
9495-- | Used for error reflection
src/Idris/IdeSlave.hs+1
@@ -89,6 +89,7 @@ instance SExpable OutputAnnotation where
8989 (SymbolAtom "implicit", BoolAtom imp)]
9090 toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]
9191 toSExp AnnConstType = toSExp [(SymbolAtom "decor", SymbolAtom "type")]
92+ toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]
9293 toSExp (AnnFC (FC f (sl, sc) (el, ec))) = toSExp [(SymbolAtom "source-loc",
9394 ((SymbolAtom "filename", StringAtom f),
9495 (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),