09f56a7 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+4−4

compare with master

unifiedsplit

@@ -871,7 +871,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

871 | PNoImplicits PTerm -- ^ never run implicit converions on the term

872 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])

873 | PUnquote PTerm -- ^ ~Term

874− | PQuoteName Name -- ^ `{n}

874+ | PQuoteName Name FC -- ^ `{n} where the FC is the precise highlighting for the name in particular

875 | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.

876 deriving (Eq, Data, Typeable)

877

@@ -931,7 +931,7 @@ mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)

931mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)

932mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)

933mapPTermFC 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)

935

936{-!

937dg instance Binary PTerm

@@ -1156,7 +1156,7 @@ highestFC (PUnifyLog tm) = highestFC tm

1156highestFC (PNoImplicits tm) = highestFC tm

1157highestFC (PQuasiquote _ _) = Nothing

1158highestFC (PUnquote tm) = highestFC tm

1159−highestFC (PQuoteName _) = Nothing

1159+highestFC (PQuoteName _ fc) = Just fc

1160highestFC (PRunElab fc _ _) = Just fc

1161highestFC (PAppImpl t _) = highestFC t

1162

@@ -1744,7 +1744,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1744 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"

1745 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"

1746 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 "}"

1748 prettySe d p bnd (PRunElab _ tm _) =

1749 bracket p funcAppPrec . group . align . hang 2 $

1750 text "%runElab" <$>

src/Idris/DeepSeq.hs+1−1

@@ -268,7 +268,7 @@ instance NFData PTerm where

268 rnf (PNoImplicits x1) = rnf x1 `seq` ()

269 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

270 rnf (PUnquote x1) = rnf x1 `seq` ()

271− rnf (PQuoteName x1) = rnf x1 `seq` ()

271+ rnf (PQuoteName x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

272 rnf (PRunElab x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

273

274instance NFData PAltType where

src/Idris/Elab/Term.hs+5−2

@@ -1106,15 +1106,18 @@ elab ist info emode opts fn tm

1106

1107

1108 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"

1109− elab' ina fc (PQuoteName n) =

1109+ elab' ina fc (PQuoteName n nfc) =

1110 do ctxt <- get_context

1111 env <- get_env

1112 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)

1114 Nothing ->

1116 Nothing ->

1115 case lookupNameDef n ctxt of

1117 case lookupNameDef n ctxt of

1116 [(n', _)] -> do fill $ reflectName n'

1118 [(n', _)] -> do fill $ reflectName n'

1117 solve

1119 solve

1120+ highlightSource nfc (AnnName n' Nothing Nothing Nothing)

1118 [] -> lift . tfail . NoSuchVariable $ n

1121 [] -> lift . tfail . NoSuchVariable $ n

1119 more -> lift . tfail . CantResolveAlts $ map fst more

1122 more -> lift . tfail . CantResolveAlts $ map fst more

1120 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"

1123 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

147warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>

148 Foldable.mapM_ (warnDisamb ist) goal

149warnDisamb ist (PUnquote tm) = warnDisamb ist tm

150−warnDisamb ist (PQuoteName _) = return ()

150+warnDisamb ist (PQuoteName _ _) = return ()

151warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm

152warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm

153warnDisamb ist (PRunElab _ tm _) = warnDisamb ist tm

src/Idris/IBC.hs+6−4

@@ -41,7 +41,7 @@ import Codec.Archive.Zip

41import Util.Zlib (decompressEither)

42

43ibcVersion :: Word16

44−ibcVersion = 113

44+ibcVersion = 114

45

46data IBCFile = IBCFile { ver :: Word16,

47 sourcefile :: FilePath,

@@ -1640,8 +1640,9 @@ instance Binary PTerm where

1640 put x2

1641 PUnquote x1 -> do putWord8 43

1642 put x1

1643− PQuoteName x1 -> do putWord8 44

1643+ PQuoteName x1 x2 -> do putWord8 44

1644− put x1

1644+ put x1

1645+ put x2

1645 PIfThenElse x1 x2 x3 x4 -> do putWord8 45

1646 PIfThenElse x1 x2 x3 x4 -> do putWord8 45

1646 put x1

1647 put x1

1647 put x2

1648 put x2

@@ -1778,7 +1779,8 @@ instance Binary PTerm where

1778 43 -> do x1 <- get

1779 43 -> do x1 <- get

1779 return (PUnquote x1)

1780 return (PUnquote x1)

1780 44 -> do x1 <- get

1781 44 -> do x1 <- get

1782+ x2 <- get

1781− return (PQuoteName x1)

1783+ return (PQuoteName x1 x2)

1782 45 -> do x1 <- get

1784 45 -> do x1 <- get

1783 x2 <- get

1785 x2 <- get

1784 x3 <- get

1786 x3 <- get

src/Idris/ParseExpr.hs+9−4

@@ -684,10 +684,15 @@ unquote syn = do guard (syn_in_quasiquote syn > 0)

684

685-}

686namequote :: SyntaxInfo -> IdrisParser PTerm

687−namequote syn = do symbol "`{"

687+namequote syn = do startFC <- symbolFC "`{"

688− n <- fst <$> fnName

688+ (n, nfc) <- fnName

689− symbol "}"

689+ endFC <- symbolFC "}"

690+ mapM_ (uncurry highlightP)

691+ [ (startFC, AnnKeyword)

692+ , (endFC, AnnKeyword)

693+ , (spanFC startFC endFC, AnnQuasiquote)

694+ ]

690− return $ PQuoteName n

695+ return $ PQuoteName n nfc

691 <?> "quoted name"

696 <?> "quoted name"

692

697

693

698