git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3826 from david-christiansen/feature/present-names

Support presentations of abstract names in output

commit50b1b41923829cdfae5a863fecd751e04d96791c authorDavid Christiansen <david@davidchristiansen.dk> dateMon 22 May 2017, 07:27 (9 years ago) parentffd2db06e13c82
3 files changed+26−1
compare with master
unifiedsplit
CHANGELOG.md+4 src/Idris/IdeMode.hs+8−1 src/Idris/REPL.hs+14
CHANGELOG.md+4
@@ -1,3 +1,7 @@
1++ Names are now annotated with their representations over the IDE
2+ protocol, which allows IDEs to provide commands that work on special
3+ names that don't have syntax, such as case block names.
4+
15# New in 1.0
26
37+ It's about time
src/Idris/IdeMode.hs+8−1
@@ -128,7 +128,8 @@ namespaceOf _ = Nothing
128128
129129instance SExpable OutputAnnotation where
130130 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),
131− (SymbolAtom "implicit", BoolAtom False)] ++
131+ (SymbolAtom "implicit", BoolAtom False),
132+ (SymbolAtom "key", StringAtom (encodeName n))] ++
132133 maybeProps [("decor", ty)] ++
133134 maybeProps [("doc-overview", d), ("type", t)] ++
134135 maybeProps [("namespace", namespaceOf n)]
@@ -172,6 +173,12 @@ instance SExpable OutputAnnotation where
172173 toSExp AnnQuasiquote = toSExp [(SymbolAtom "quasiquotation", True)]
173174 toSExp AnnAntiquote = toSExp [(SymbolAtom "antiquotation", True)]
174175
176+encodeName :: Name -> String
177+encodeName n = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ n
178+
179+decodeName :: String -> Name
180+decodeName = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
181+
175182encodeTerm :: [(Name, Bool)] -> Term -> String
176183encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $
177184 (bnd, tm)
src/Idris/REPL.hs+14
@@ -26,6 +26,10 @@ import Control.Monad
2626import Control.Monad.Trans (lift)
2727import Control.Monad.Trans.Except (runExceptT)
2828import Control.Monad.Trans.State.Strict (evalStateT, get, put)
29+import qualified Data.Binary as Binary
30+import qualified Data.ByteString.Base64 as Base64
31+import qualified Data.ByteString.Lazy as Lazy
32+import qualified Data.ByteString.UTF8 as UTF8
2933import Data.Char
3034import Data.Either (partitionEithers)
3135import Data.List hiding (group)
@@ -582,6 +586,16 @@ ideModeForceTermImplicits h id bnd impl tm =
582586 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
583587
584588splitName :: String -> Either String Name
589+splitName s | "{{{{{" `isPrefixOf` s =
590+ decode $ drop 5 $ reverse $ drop 5 $ reverse s
591+ where decode x =
592+ case Base64.decode (UTF8.fromString x) of
593+ Left err -> Left err
594+ Right ok ->
595+ case Binary.decodeOrFail (Lazy.fromStrict ok) of
596+ Left _ -> Left "Bad binary instance for Name"
597+ Right (_, _, n) -> Right n
598+
585599splitName s = case reverse $ splitOn "." s of
586600 [] -> Left ("Didn't understand name '" ++ s ++ "'")
587601 [n] -> Right . sUN $ unparen n