git.iko.soy/Idris-dev
on master help sign in
Add ppOptionIst function.
9491c3cPeter Minten
src/Idris/AbsSyntaxTree.hs+6−2
compare with master
unifiedsplit
@@ -113,6 +113,10 @@ ppOption opt = PPOption {
113 ppopt_impl = opt_showimp opt
113 ppopt_impl = opt_showimp opt
114}
114}
115
115
116+-- | Get pretty printing options from an idris state record.
117+ppOptionIst :: IState -> PPOption
118+ppOptionIst = ppOption . idris_options
119+
116data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
120data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
117
121
118-- | The output mode in use
122-- | The output mode in use
@@ -1154,7 +1158,7 @@ prettyImp impl = pprintPTerm impl [] [] []
1154
1158
1155-- | Do the right thing for rendering a term in an IState
1159-- | Do the right thing for rendering a term in an IState
1156prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1160prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1157−prettyIst ist = pprintPTerm (ppOption (idris_options ist)) [] [] (idris_infixes ist)
1161+prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1158
1162
1159-- | Pretty-print a high-level Idris term in some bindings context with infix info
1163-- | Pretty-print a high-level Idris term in some bindings context with infix info
1160pprintPTerm :: PPOption -- ^^ pretty printing options
1164pprintPTerm :: PPOption -- ^^ pretty printing options
@@ -1527,7 +1531,7 @@ showTm :: IState -- ^^ the Idris state, for information about identifiers and co
1527 -> String
1531 -> String
1528showTm ist = displayDecorated (consoleDecorate ist) .
1532showTm ist = displayDecorated (consoleDecorate ist) .
1529 renderPretty 0.8 100000 .
1533 renderPretty 0.8 100000 .
1530− prettyImp (ppOption (idris_options ist))
1534+ prettyImp (ppOptionIst ist)
1531
1535
1532-- | Show a term with implicits, no colours
1536-- | Show a term with implicits, no colours
1533showTmImpls :: PTerm -> String
1537showTmImpls :: PTerm -> String
src/Idris/Delaborate.hs+2−2
@@ -138,7 +138,7 @@ pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
138pprintTerm ist = pprintTerm' ist []
138pprintTerm ist = pprintTerm' ist []
139
139
140pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
140pprintTerm' :: 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
142
142
143pprintErr :: IState -> Err -> Doc OutputAnnotation
143pprintErr :: IState -> Err -> Doc OutputAnnotation
144pprintErr i err = pprintErr' i (fmap (errReverse i) err)
144pprintErr i err = pprintErr' i (fmap (errReverse i) err)
@@ -269,7 +269,7 @@ showSc i xs = line <> line <> text "In context:" <>
269
269
270
270
271showqual :: IState -> Name -> String
271showqual :: 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)
273 where
273 where
274 dens ns@(NS n _) = case lookupCtxt n (idris_implicits i) of
274 dens ns@(NS n _) = case lookupCtxt n (idris_implicits i) of
275 [_] -> n -- just one thing
275 [_] -> n -- just one thing
src/Idris/Docs.hs+2−2
@@ -46,7 +46,7 @@ pprintFD ist (FD n doc args ty f)
46 then nest 4 $ text "Arguments:" <$> vsep argshow
46 then nest 4 $ text "Arguments:" <$> vsep argshow
47 else empty)
47 else empty)
48
48
49− where ppo = ppOption (idris_options ist)
49+ where ppo = ppOptionIst ist
50 infixes = idris_infixes ist
50 infixes = idris_infixes ist
51 showArgs ((n, ty, Exp {}, Just d):args) bnd
51 showArgs ((n, ty, Exp {}, Just d):args) bnd
52 = bindingOf n False <+> colon <+>
52 = bindingOf n False <+> colon <+>
@@ -97,7 +97,7 @@ pprintDocs ist (ClassDoc n doc meths params instances)
97
97
98 pNames = map fst params
98 pNames = map fst params
99
99
100− ppo = ppOption (idris_options ist)
100+ ppo = ppOptionIst ist
101 infixes = idris_infixes ist
101 infixes = idris_infixes ist
102
102
103 dumpInstance :: PTerm -> Doc OutputAnnotation
103 dumpInstance :: PTerm -> Doc OutputAnnotation
src/Idris/Output.hs+2−2
@@ -87,7 +87,7 @@ ihPrintTermWithType h tm ty = do ist <- getIState
87ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
87ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
88ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n
88ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n
89ihPrintFunTypes h bnd n overloads = do ist <- getIState
89ihPrintFunTypes h bnd n overloads = do ist <- getIState
90− let ppo = ppOption (idris_options ist)
90+ let ppo = ppOptionIst ist
91 let infixes = idris_infixes ist
91 let infixes = idris_infixes ist
92 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
92 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
93 case idris_outputmode ist of
93 case idris_outputmode ist of
@@ -121,7 +121,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =
121 out = displayS . renderPretty 1.0 50 $ renderDocstring o
121 out = displayS . renderPretty 1.0 50 $ renderDocstring o
122 return (out "")
122 return (out "")
123 getTy :: IState -> Name -> String -- fails if name not already extant!
123 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) $
125 delabTy ist n
125 delabTy ist n
126 in (displayS . renderPretty 1.0 50 $ theTy) ""
126 in (displayS . renderPretty 1.0 50 $ theTy) ""
127fancifyAnnots _ annot = annot
127fancifyAnnots _ annot = annot
src/Idris/Prover.hs+2−2
@@ -110,7 +110,7 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =
110 iputGoal rendered
110 iputGoal rendered
111
111
112 where
112 where
113− ppo = ppOption (idris_options ist)
113+ ppo = ppOptionIst ist
114
114
115 tPretty bnd t = pprintPTerm ppo bnd [] (idris_infixes ist) $ delab ist t
115 tPretty bnd t = pprintPTerm ppo bnd [] (idris_infixes ist) $ delab ist t
116
116
@@ -237,7 +237,7 @@ ploop fn d prompt prf e h
237 ctxt' = envCtxt env ctxt
237 ctxt' = envCtxt env ctxt
238 putIState ist { tt_ctxt = ctxt' }
238 putIState ist { tt_ctxt = ctxt' }
239 (tm, ty) <- elabVal toplevel False t
239 (tm, ty) <- elabVal toplevel False t
240− let ppo = ppOption (idris_options ist)
240+ let ppo = ppOptionIst ist
241 ty' = normaliseC ctxt [] ty
241 ty' = normaliseC ctxt [] ty
242 h = idris_outh ist
242 h = idris_outh ist
243 infixes = idris_infixes ist
243 infixes = idris_infixes ist
src/Idris/REPL.hs+5−5
@@ -312,7 +312,7 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =
312runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
312runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
313 do ist <- getIState
313 do ist <- getIState
314 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
314 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
315− let ppo = ppOption (idris_options ist)
315+ let ppo = ppOptionIst ist
316 let mvarTys = map (delabTy ist) mvs
316 let mvarTys = map (delabTy ist) mvs
317 let res = (IdeSlave.SymbolAtom "ok",
317 let res = (IdeSlave.SymbolAtom "ok",
318 zipWith (\ n (prems, concl) -> (n, prems, concl))
318 zipWith (\ n (prems, concl) -> (n, prems, concl))
@@ -581,7 +581,7 @@ process h fn (ExecVal t)
581process h fn (Check (PRef _ n))
581process h fn (Check (PRef _ n))
582 = do ctxt <- getContext
582 = do ctxt <- getContext
583 ist <- getIState
583 ist <- getIState
584− let ppo = ppOption (idris_options ist)
584+ let ppo = ppOptionIst ist
585 case lookupNames n ctxt of
585 case lookupNames n ctxt of
586 ts@(t:_) ->
586 ts@(t:_) ->
587 case lookup t (idris_metavars ist) of
587 case lookup t (idris_metavars ist) of
@@ -610,14 +610,14 @@ process h fn (Check (PRef _ n))
610 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
610 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
611 align (tPretty bnd ist g)
611 align (tPretty bnd ist g)
612
612
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
614
614
615
615
616process h fn (Check t)
616process h fn (Check t)
617 = do (tm, ty) <- elabVal toplevel False t
617 = do (tm, ty) <- elabVal toplevel False t
618 ctxt <- getContext
618 ctxt <- getContext
619 ist <- getIState
619 ist <- getIState
620− let ppo = ppOption (idris_options ist)
620+ let ppo = ppOptionIst ist
621 ty' = normaliseC ctxt [] ty
621 ty' = normaliseC ctxt [] ty
622 case tm of
622 case tm of
623 TType _ ->
623 TType _ ->
@@ -664,7 +664,7 @@ process h fn (TotCheck n)
664 [] -> ihPrintError h $ "Unknown operator " ++ show n
664 [] -> ihPrintError h $ "Unknown operator " ++ show n
665 ts -> do ist <- getIState
665 ts -> do ist <- getIState
666 c <- colourise
666 c <- colourise
667− let ppo = ppOption (idris_options ist)
667+ let ppo = ppOptionIst ist
668 let showN = showName (Just ist) [] ppo c
668 let showN = showName (Just ist) [] ppo c
669 ihPrintResult h . concat . intersperse "\n" .
669 ihPrintResult h . concat . intersperse "\n" .
670 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
670 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $