@@ -84,8 +84,7 @@ dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) = do
8484 prettyG b = tPretty $ binderTy b
8585
8686 prettyGoal ty =
87− text "----------" <+> text "Metavariable currently in focus" <> colon
88− <+> pretty nm <+> text "----------" $$
87+ text "---------- Goal: ----------" $$
8988 pretty h <> colon $$ nest nestingSize (prettyG ty)
9089
9190 prettyAssumptions env =
@@ -102,34 +101,6 @@ dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) = do
102101 text "---------- Other goals: ----------" $$
103102 pretty hs
104103
105−
106−{-
107−dumpState :: IState -> ProofState -> IO ()
108−dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
109−dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)
110− = do let OK ty = goalAtFocus ps
111− let OK env = envAtFocus ps
112−-- putStrLn $ "Other goals: " ++ show hs ++ "\n"
113− putStr $ "\n" ++ showPs (reverse env)
114− putStrLn $ "---------------------------------- (" ++ show nm
115− ++ ") --------"
116− putStrLn $ show h ++ " : " ++ showG ty ++ "\n"
117− where
118− tshow t = show (delab ist t)
119−
120− showPs [] = ""
121− showPs ((MN _ "rewrite_rule", _) : bs) = showPs bs
122− showPs ((n, Let t v) : bs)
123− = " " ++ show n ++ " = " ++ tshow v ++ " : " ++
124− tshow t ++ "\n" ++ showPs bs
125− showPs ((n, b) : bs)
126− = " " ++ show n ++ " : " ++
127− tshow (binderTy b) ++ "\n" ++ showPs bs
128−
129− showG (Guess t v) = tshow t ++ " =?= " ++ tshow v
130− showG b = tshow (binderTy b)
131−-}
132−
133104lifte :: ElabState [PDecl] -> ElabD a -> Idris a
134105lifte st e = do (v, _) <- elabStep st e
135106 return v