Skip to content

Commit

Permalink
Indentation improvement
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed May 18, 2015
1 parent 0696537 commit b643b7a
Showing 1 changed file with 11 additions and 11 deletions.
22 changes: 11 additions & 11 deletions src/Idris/REPL.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit b643b7a

Please sign in to comment.