git.iko.soy/Idris-dev
on master help sign in
Add IDE command for showing TT

This enables interactions in IDEs such as right-clicking terms in error messages to see the corresponding TT terms, similar to the implicits and normalisation commands.

commit6c26814d08390b956d8d56806096c8f14955560e authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 16 Mar 2015, 20:30 (12 years ago) parent01c4f2a
3 files changed+15−1
compare with master
unifiedsplit
CHANGELOG+3−1 src/Idris/IdeMode.hs+3 src/Idris/REPL.hs+9
CHANGELOG+3−1
@@ -30,7 +30,9 @@ New in 0.9.17:
3030* Unification errors now (where possible) contain information about provenance
3131 of a type
3232* New REPL command ":core TM" that shows the elaborated form of TM along with
33− its elaborated type using the syntax of TT
33+ its elaborated type using the syntax of TT. IDE mode has a corresponding
34+ command :elaborate-term for serialized terms.
35+
3436
3537New in 0.9.16:
3638--------------
src/Idris/IdeMode.hs+3
@@ -229,6 +229,7 @@ data IdeModeCommand = REPLCompletions String
229229 | TermNormalise [(Name, Bool)] Term
230230 | TermShowImplicits [(Name, Bool)] Term
231231 | TermNoImplicits [(Name, Bool)] Term
232+ | TermElab [(Name, Bool)] Term
232233 | PrintDef String
233234 | ErrString Err
234235 | ErrPPrint Err
@@ -278,6 +279,8 @@ sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded])
278279 Just (TermShowImplicits bnd tm)
279280sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
280281 Just (TermNoImplicits bnd tm)
282+sexpToCommand (SexpList [SymbolAtom "elaborate-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
283+ Just (TermElab bnd tm)
281284sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)
282285sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded
283286sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded]) = Just . ErrPPrint . decodeErr $ encoded
src/Idris/REPL.hs+9
@@ -494,6 +494,15 @@ runIdeModeCommand h id orig fn modes (IdeMode.TermShowImplicits bnd tm) =
494494 ideModeForceTermImplicits h id bnd True tm
495495runIdeModeCommand h id orig fn modes (IdeMode.TermNoImplicits bnd tm) =
496496 ideModeForceTermImplicits h id bnd False tm
497+runIdeModeCommand h id orig fn modes (IdeMode.TermElab bnd tm) =
498+ do ist <- getIState
499+ let ptm = annotate (AnnTerm bnd tm)
500+ (pprintTT (map fst bnd) tm)
501+ msg = (IdeMode.SymbolAtom "ok",
502+ displaySpans .
503+ renderPretty 0.9 70 .
504+ fmap (fancifyAnnots ist) $ ptm)
505+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
497506runIdeModeCommand h id orig fn mods (IdeMode.PrintDef name) =
498507 case splitName name of
499508 Left err -> iPrintError err