From b643b7a9837a361f1c7aa1d7ad40cb5e1633a08c Mon Sep 17 00:00:00 2001 From: David Raymond Christiansen Date: Mon, 18 May 2015 16:33:21 +0200 Subject: [PATCH] Indentation improvement --- src/Idris/REPL.hs | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs index a4d28be437..704bd94df7 100644 --- a/src/Idris/REPL.hs +++ b/src/Idris/REPL.hs @@ -990,17 +990,17 @@ process fn (Defn n) in text (showTm i' (delab i lhs)) <+> text "=" <+> text (showTm i' (delab i rhs)) process fn (TotCheck n) - = do i <- getIState - case lookupNameTotal n (tt_ctxt i) of - [] -> iPrintError $ "Unknown operator " ++ show n - ts -> do ist <- getIState - c <- colourise - let ppo = ppOptionIst ist - let showN n = annotate (AnnName n Nothing Nothing Nothing) . text $ - showName (Just ist) [] ppo False n - iRenderResult . vsep . - map (\(n, t) -> hang 4 $ showN n <+> text "is" <+> showTotal t i) $ - ts + = do i <- getIState + case lookupNameTotal n (tt_ctxt i) of + [] -> iPrintError $ "Unknown operator " ++ show n + ts -> do ist <- getIState + c <- colourise + let ppo = ppOptionIst ist + let showN n = annotate (AnnName n Nothing Nothing Nothing) . text $ + showName (Just ist) [] ppo False n + iRenderResult . vsep . + map (\(n, t) -> hang 4 $ showN n <+> text "is" <+> showTotal t i) $ + ts process fn (DebugUnify l r) = do (ltm, _) <- elabVal recinfo ERHS l