git.iko.soy/Idris-dev
on master help sign in
Add ppOptionIst function.
commit9491c3c397a79118cea0b9605d2eccf9a4a52ce1 authorPeter Minten <peter.minten@online.nl> dateSat 3 May 2014, 18:36 (12 years ago) parent5e3c248
6 files changed+19−15
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+6−2 src/Idris/Delaborate.hs+2−2 src/Idris/Docs.hs+2−2 src/Idris/Output.hs+2−2 src/Idris/Prover.hs+2−2 src/Idris/REPL.hs+5−5
src/Idris/AbsSyntaxTree.hs+6−2
@@ -113,6 +113,10 @@ ppOption opt = PPOption {
113113 ppopt_impl = opt_showimp opt
114114}
115115
116+-- | Get pretty printing options from an idris state record.
117+ppOptionIst :: IState -> PPOption
118+ppOptionIst = ppOption . idris_options
119+
116120data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
117121
118122-- | The output mode in use
@@ -1154,7 +1158,7 @@ prettyImp impl = pprintPTerm impl [] [] []
11541158
11551159-- | Do the right thing for rendering a term in an IState
11561160prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1157−prettyIst ist = pprintPTerm (ppOption (idris_options ist)) [] [] (idris_infixes ist)
1161+prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
11581162
11591163-- | Pretty-print a high-level Idris term in some bindings context with infix info
11601164pprintPTerm :: PPOption -- ^^ pretty printing options
@@ -1527,7 +1531,7 @@ showTm :: IState -- ^^ the Idris state, for information about identifiers and co
15271531 -> String
15281532showTm ist = displayDecorated (consoleDecorate ist) .
15291533 renderPretty 0.8 100000 .
1530− prettyImp (ppOption (idris_options ist))
1534+ prettyImp (ppOptionIst ist)
15311535
15321536-- | Show a term with implicits, no colours
15331537showTmImpls :: PTerm -> String
src/Idris/Delaborate.hs+2−2
@@ -138,7 +138,7 @@ pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
138138pprintTerm ist = pprintTerm' ist []
139139
140140pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
141−pprintTerm' ist bnd tm = pprintPTerm (ppOption (idris_options ist)) bnd [] (idris_infixes ist) tm
141+pprintTerm' ist bnd tm = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) tm
142142
143143pprintErr :: IState -> Err -> Doc OutputAnnotation
144144pprintErr i err = pprintErr' i (fmap (errReverse i) err)
@@ -269,7 +269,7 @@ showSc i xs = line <> line <> text "In context:" <>
269269
270270
271271showqual :: IState -> Name -> String
272−showqual i n = showName (Just i) [] (ppOption (idris_options i)) { ppopt_impl = False } False (dens n)
272+showqual i n = showName (Just i) [] (ppOptionIst i) { ppopt_impl = False } False (dens n)
273273 where
274274 dens ns@(NS n _) = case lookupCtxt n (idris_implicits i) of
275275 [_] -> n -- just one thing
src/Idris/Docs.hs+2−2
@@ -46,7 +46,7 @@ pprintFD ist (FD n doc args ty f)
4646 then nest 4 $ text "Arguments:" <$> vsep argshow
4747 else empty)
4848
49− where ppo = ppOption (idris_options ist)
49+ where ppo = ppOptionIst ist
5050 infixes = idris_infixes ist
5151 showArgs ((n, ty, Exp {}, Just d):args) bnd
5252 = bindingOf n False <+> colon <+>
@@ -97,7 +97,7 @@ pprintDocs ist (ClassDoc n doc meths params instances)
9797
9898 pNames = map fst params
9999
100− ppo = ppOption (idris_options ist)
100+ ppo = ppOptionIst ist
101101 infixes = idris_infixes ist
102102
103103 dumpInstance :: PTerm -> Doc OutputAnnotation
src/Idris/Output.hs+2−2
@@ -87,7 +87,7 @@ ihPrintTermWithType h tm ty = do ist <- getIState
8787ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
8888ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n
8989ihPrintFunTypes h bnd n overloads = do ist <- getIState
90− let ppo = ppOption (idris_options ist)
90+ let ppo = ppOptionIst ist
9191 let infixes = idris_infixes ist
9292 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
9393 case idris_outputmode ist of
@@ -121,7 +121,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =
121121 out = displayS . renderPretty 1.0 50 $ renderDocstring o
122122 return (out "")
123123 getTy :: IState -> Name -> String -- fails if name not already extant!
124− getTy ist n = let theTy = pprintPTerm (ppOption (idris_options ist)) [] [] (idris_infixes ist) $
124+ getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
125125 delabTy ist n
126126 in (displayS . renderPretty 1.0 50 $ theTy) ""
127127fancifyAnnots _ annot = annot
src/Idris/Prover.hs+2−2
@@ -110,7 +110,7 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =
110110 iputGoal rendered
111111
112112 where
113− ppo = ppOption (idris_options ist)
113+ ppo = ppOptionIst ist
114114
115115 tPretty bnd t = pprintPTerm ppo bnd [] (idris_infixes ist) $ delab ist t
116116
@@ -237,7 +237,7 @@ ploop fn d prompt prf e h
237237 ctxt' = envCtxt env ctxt
238238 putIState ist { tt_ctxt = ctxt' }
239239 (tm, ty) <- elabVal toplevel False t
240− let ppo = ppOption (idris_options ist)
240+ let ppo = ppOptionIst ist
241241 ty' = normaliseC ctxt [] ty
242242 h = idris_outh ist
243243 infixes = idris_infixes ist
src/Idris/REPL.hs+5−5
@@ -312,7 +312,7 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =
312312runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
313313 do ist <- getIState
314314 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
315− let ppo = ppOption (idris_options ist)
315+ let ppo = ppOptionIst ist
316316 let mvarTys = map (delabTy ist) mvs
317317 let res = (IdeSlave.SymbolAtom "ok",
318318 zipWith (\ n (prems, concl) -> (n, prems, concl))
@@ -581,7 +581,7 @@ process h fn (ExecVal t)
581581process h fn (Check (PRef _ n))
582582 = do ctxt <- getContext
583583 ist <- getIState
584− let ppo = ppOption (idris_options ist)
584+ let ppo = ppOptionIst ist
585585 case lookupNames n ctxt of
586586 ts@(t:_) ->
587587 case lookup t (idris_metavars ist) of
@@ -610,14 +610,14 @@ process h fn (Check (PRef _ n))
610610 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
611611 align (tPretty bnd ist g)
612612
613− tPretty bnd ist t = pprintPTerm (ppOption (idris_options ist)) bnd [] (idris_infixes ist) t
613+ tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t
614614
615615
616616process h fn (Check t)
617617 = do (tm, ty) <- elabVal toplevel False t
618618 ctxt <- getContext
619619 ist <- getIState
620− let ppo = ppOption (idris_options ist)
620+ let ppo = ppOptionIst ist
621621 ty' = normaliseC ctxt [] ty
622622 case tm of
623623 TType _ ->
@@ -664,7 +664,7 @@ process h fn (TotCheck n)
664664 [] -> ihPrintError h $ "Unknown operator " ++ show n
665665 ts -> do ist <- getIState
666666 c <- colourise
667− let ppo = ppOption (idris_options ist)
667+ let ppo = ppOptionIst ist
668668 let showN = showName (Just ist) [] ppo c
669669 ihPrintResult h . concat . intersperse "\n" .
670670 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $