git.iko.soy/Idris-dev
on master help sign in
Add IDE command for showing TT
6c26814David Raymond Christiansen
CHANGELOG+3−1
compare with master
unifiedsplit
@@ -30,7 +30,9 @@ New in 0.9.17:
30* Unification errors now (where possible) contain information about provenance
30* Unification errors now (where possible) contain information about provenance
31 of a type
31 of a type
32* New REPL command ":core TM" that shows the elaborated form of TM along with
32* 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+
34
36
35New in 0.9.16:
37New in 0.9.16:
36--------------
38--------------
src/Idris/IdeMode.hs+3
@@ -229,6 +229,7 @@ data IdeModeCommand = REPLCompletions String
229 | TermNormalise [(Name, Bool)] Term
229 | TermNormalise [(Name, Bool)] Term
230 | TermShowImplicits [(Name, Bool)] Term
230 | TermShowImplicits [(Name, Bool)] Term
231 | TermNoImplicits [(Name, Bool)] Term
231 | TermNoImplicits [(Name, Bool)] Term
232+ | TermElab [(Name, Bool)] Term
232 | PrintDef String
233 | PrintDef String
233 | ErrString Err
234 | ErrString Err
234 | ErrPPrint Err
235 | ErrPPrint Err
@@ -278,6 +279,8 @@ sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded])
278 Just (TermShowImplicits bnd tm)
279 Just (TermShowImplicits bnd tm)
279sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
280sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
280 Just (TermNoImplicits bnd tm)
281 Just (TermNoImplicits bnd tm)
282+sexpToCommand (SexpList [SymbolAtom "elaborate-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
283+ Just (TermElab bnd tm)
281sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)
284sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)
282sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded
285sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded
283sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded]) = Just . ErrPPrint . decodeErr $ encoded
286sexpToCommand (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) =
494 ideModeForceTermImplicits h id bnd True tm
494 ideModeForceTermImplicits h id bnd True tm
495runIdeModeCommand h id orig fn modes (IdeMode.TermNoImplicits bnd tm) =
495runIdeModeCommand h id orig fn modes (IdeMode.TermNoImplicits bnd tm) =
496 ideModeForceTermImplicits h id bnd False tm
496 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
497runIdeModeCommand h id orig fn mods (IdeMode.PrintDef name) =
506runIdeModeCommand h id orig fn mods (IdeMode.PrintDef name) =
498 case splitName name of
507 case splitName name of
499 Left err -> iPrintError err
508 Left err -> iPrintError err