git.iko.soy/Idris-dev
on master help sign in
Use pretty-printer to display :t for metavars
commit106061dccdb0f47236949dbeed6705600035002b authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 31 Jan 2014, 22:07 (13 years ago) parent41d3daf
2 files changed+31−21
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+9−3 src/Idris/REPL.hs+22−18
src/Idris/AbsSyntax.hs+9−3
@@ -417,9 +417,9 @@ setWidth w = do ist <- getIState
417417iRender :: Doc a -> Idris (SimpleDoc a)
418418iRender d = do w <- getWidth
419419 return $ case w of
420− InfinitelyWide -> renderCompact d
420+ InfinitelyWide -> renderPretty 1.0 1000000000 d
421421 ColsWide n -> if n < 1
422− then renderCompact d
422+ then renderPretty 1.0 1000000000 d
423423 else renderPretty 0.5 n d
424424
425425ihPrintResult :: Handle -> String -> Idris ()
@@ -445,7 +445,7 @@ consoleDisplayAnnotated h output = do ist <- getIState
445445ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
446446ideSlaveReturnAnnotated n h out = do ist <- getIState
447447 let (str, spans) = displaySpans .
448− renderCompact .
448+ renderPretty 0.8 80 .
449449 fmap (fancifyAnnots ist) $
450450 out
451451 good = [SymbolAtom "ok", toSExp str, toSExp spans]
@@ -470,6 +470,12 @@ ihPrintFunTypes h n overloads = do imp <- impShow
470470 where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)
471471 ppOverload imp n tm = fullName n <+> colon <+> align (prettyImp imp tm)
472472
473+ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
474+ihRenderResult h d = do ist <- getIState
475+ case idris_outputmode ist of
476+ RawOutput -> consoleDisplayAnnotated h d
477+ IdeSlave n -> ideSlaveReturnAnnotated n h d
478+
473479fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
474480fancifyAnnots ist annot@(AnnName n _ _) =
475481 do let ctxt = tt_ctxt ist
src/Idris/REPL.hs+22−18
@@ -14,7 +14,7 @@ import Idris.Parser
1414import Idris.Primitives
1515import Idris.Coverage
1616import Idris.UnusedArgs
17−import Idris.Docs
17+import Idris.Docs hiding (Doc)
1818import Idris.Help
1919import Idris.Completion
2020import qualified Idris.IdeSlave as IdeSlave
@@ -30,6 +30,7 @@ import Version_idris (gitHash)
3030import Util.System
3131import Util.DynamicLinker
3232import Util.Net (listenOnLocalhost)
33+import Util.Pretty hiding ((</>))
3334
3435import Idris.Core.Evaluate
3536import Idris.Core.Execute (execute)
@@ -470,32 +471,35 @@ process h fn (Check (PRef _ n))
470471 = do ctxt <- getContext
471472 ist <- getIState
472473 imp <- impShow
473− c <- colourise
474474 case lookupNames n ctxt of
475475 ts@(t:_) ->
476476 case lookup t (idris_metavars ist) of
477− Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)
477+ Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $
478+ showMetavarInfo imp ist n i
478479 Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)
479480 [] -> ihPrintError h $ "No such variable " ++ show n
480481 where
481− showMetavarInfo c imp ist n i
482+ showMetavarInfo imp ist n i
482483 = case lookupTy n (tt_ctxt ist) of
483− (ty:_) -> putTy c imp ist i (delab ist ty)
484− putTy c imp ist 0 sc = putGoal c imp ist sc
485− putTy c imp ist i (PPi _ n t sc)
486− = let current = " " ++
484+ (ty:_) -> putTy imp ist i [] (delab ist ty)
485+ putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
486+ putTy imp ist 0 bnd sc = putGoal imp ist bnd sc
487+ putTy imp ist i bnd (PPi _ n t sc)
488+ = let current = text " " <>
487489 (case n of
488− MN _ _ -> "_"
489− UN nm | ('_':'_':_) <- str nm -> "_"
490− _ -> showName (Just ist) [] False c n) ++
491− " : " ++ showTm ist t ++ "\n"
490+ MN _ _ -> text "_"
491+ UN nm | ('_':'_':_) <- str nm -> text "_"
492+ _ -> bindingOf n False) <+>
493+ colon <+> align (tPretty bnd ist t) <> line
492494 in
493− current ++ putTy c imp ist (i-1) sc
494− putTy c imp ist _ sc = putGoal c imp ist sc
495− putGoal c imp ist g
496− = "--------------------------------------\n" ++
497− showName (Just ist) [] False c n ++ " : " ++
498− showTm ist g
495+ current <> putTy imp ist (i-1) ((n,False):bnd) sc
496+ putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc
497+ putGoal imp ist bnd g
498+ = text "--------------------------------------" <$>
499+ annotate (AnnName n Nothing Nothing) (text $ show n) <+> colon <+>
500+ align (tPretty bnd ist g)
501+
502+ tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd t
499503
500504
501505process h fn (Check t)