git.iko.soy/Idris-dev
on master help sign in
Add compiler highlighting for quoted names in source

Name quotations are now highlighted with the actual name, and the surrounding brackets are highlighted as a quotation. This can make it easier to follow reflection code.

commit09f56a721dc120dc7d0ed82774e60d7b29714486 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 10 Jul 2015, 14:18 (11 years ago) parentec0b043
6 files changed+26−16
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+4−4 src/Idris/DeepSeq.hs+1−1 src/Idris/Elab/Term.hs+5−2 src/Idris/Error.hs+1−1 src/Idris/IBC.hs+6−4 src/Idris/ParseExpr.hs+9−4
src/Idris/AbsSyntaxTree.hs+4−4
@@ -871,7 +871,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua
871871 | PNoImplicits PTerm -- ^ never run implicit converions on the term
872872 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
873873 | PUnquote PTerm -- ^ ~Term
874− | PQuoteName Name -- ^ `{n}
874+ | PQuoteName Name FC -- ^ `{n} where the FC is the precise highlighting for the name in particular
875875 | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.
876876 deriving (Eq, Data, Typeable)
877877
@@ -931,7 +931,7 @@ mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
931931mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
932932mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
933933mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
934−mapPTermFC f g (PQuoteName n) = PQuoteName n
934+mapPTermFC f g (PQuoteName n fc) = PQuoteName n (g fc)
935935
936936{-!
937937dg instance Binary PTerm
@@ -1156,7 +1156,7 @@ highestFC (PUnifyLog tm) = highestFC tm
11561156highestFC (PNoImplicits tm) = highestFC tm
11571157highestFC (PQuasiquote _ _) = Nothing
11581158highestFC (PUnquote tm) = highestFC tm
1159−highestFC (PQuoteName _) = Nothing
1159+highestFC (PQuoteName _ fc) = Just fc
11601160highestFC (PRunElab fc _ _) = Just fc
11611161highestFC (PAppImpl t _) = highestFC t
11621162
@@ -1744,7 +1744,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
17441744 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
17451745 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
17461746 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1747− prettySe d p bnd (PQuoteName n) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1747+ prettySe d p bnd (PQuoteName n _) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
17481748 prettySe d p bnd (PRunElab _ tm _) =
17491749 bracket p funcAppPrec . group . align . hang 2 $
17501750 text "%runElab" <$>
src/Idris/DeepSeq.hs+1−1
@@ -268,7 +268,7 @@ instance NFData PTerm where
268268 rnf (PNoImplicits x1) = rnf x1 `seq` ()
269269 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
270270 rnf (PUnquote x1) = rnf x1 `seq` ()
271− rnf (PQuoteName x1) = rnf x1 `seq` ()
271+ rnf (PQuoteName x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
272272 rnf (PRunElab x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
273273
274274instance NFData PAltType where
src/Idris/Elab/Term.hs+5−2
@@ -1106,15 +1106,18 @@ elab ist info emode opts fn tm
11061106
11071107
11081108 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"
1109− elab' ina fc (PQuoteName n) =
1109+ elab' ina fc (PQuoteName n nfc) =
11101110 do ctxt <- get_context
11111111 env <- get_env
11121112 case lookup n env of
1113− Just _ -> do fill $ reflectName n ; solve
1113+ Just _ -> do fill $ reflectName n
1114+ solve
1115+ highlightSource nfc (AnnBoundName n False)
11141116 Nothing ->
11151117 case lookupNameDef n ctxt of
11161118 [(n', _)] -> do fill $ reflectName n'
11171119 solve
1120+ highlightSource nfc (AnnName n' Nothing Nothing Nothing)
11181121 [] -> lift . tfail . NoSuchVariable $ n
11191122 more -> lift . tfail . CantResolveAlts $ map fst more
11201123 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"
src/Idris/Error.hs+1−1
@@ -147,7 +147,7 @@ warnDisamb ist (PNoImplicits tm) = warnDisamb ist tm
147147warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
148148 Foldable.mapM_ (warnDisamb ist) goal
149149warnDisamb ist (PUnquote tm) = warnDisamb ist tm
150−warnDisamb ist (PQuoteName _) = return ()
150+warnDisamb ist (PQuoteName _ _) = return ()
151151warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
152152warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
153153warnDisamb ist (PRunElab _ tm _) = warnDisamb ist tm
src/Idris/IBC.hs+6−4
@@ -41,7 +41,7 @@ import Codec.Archive.Zip
4141import Util.Zlib (decompressEither)
4242
4343ibcVersion :: Word16
44−ibcVersion = 113
44+ibcVersion = 114
4545
4646data IBCFile = IBCFile { ver :: Word16,
4747 sourcefile :: FilePath,
@@ -1640,8 +1640,9 @@ instance Binary PTerm where
16401640 put x2
16411641 PUnquote x1 -> do putWord8 43
16421642 put x1
1643− PQuoteName x1 -> do putWord8 44
1644− put x1
1643+ PQuoteName x1 x2 -> do putWord8 44
1644+ put x1
1645+ put x2
16451646 PIfThenElse x1 x2 x3 x4 -> do putWord8 45
16461647 put x1
16471648 put x2
@@ -1778,7 +1779,8 @@ instance Binary PTerm where
17781779 43 -> do x1 <- get
17791780 return (PUnquote x1)
17801781 44 -> do x1 <- get
1781− return (PQuoteName x1)
1782+ x2 <- get
1783+ return (PQuoteName x1 x2)
17821784 45 -> do x1 <- get
17831785 x2 <- get
17841786 x3 <- get
src/Idris/ParseExpr.hs+9−4
@@ -684,10 +684,15 @@ unquote syn = do guard (syn_in_quasiquote syn > 0)
684684
685685-}
686686namequote :: SyntaxInfo -> IdrisParser PTerm
687−namequote syn = do symbol "`{"
688− n <- fst <$> fnName
689− symbol "}"
690− return $ PQuoteName n
687+namequote syn = do startFC <- symbolFC "`{"
688+ (n, nfc) <- fnName
689+ endFC <- symbolFC "}"
690+ mapM_ (uncurry highlightP)
691+ [ (startFC, AnnKeyword)
692+ , (endFC, AnnKeyword)
693+ , (spanFC startFC endFC, AnnQuasiquote)
694+ ]
695+ return $ PQuoteName n nfc
691696 <?> "quoted name"
692697
693698