use dots for record fields
This commit is contained in:
parent
9fb4ad6657
commit
bc1aa21f09
4 changed files with 7 additions and 8 deletions
|
@ -114,11 +114,11 @@ HasEnv = MonadReader PrettyEnv
|
|||
|
||||
export
|
||||
ifUnicode : HasEnv m => (uni, asc : Lazy a) -> m a
|
||||
ifUnicode uni asc = if unicode !ask then [|uni|] else [|asc|]
|
||||
ifUnicode uni asc = if (!ask).unicode then [|uni|] else [|asc|]
|
||||
|
||||
export
|
||||
parensIfM : HasEnv m => PPrec -> Doc HL -> m (Doc HL)
|
||||
parensIfM d doc = pure $ parensIf (prec !ask > d) doc
|
||||
parensIfM d doc = pure $ parensIf ((!ask).prec > d) doc
|
||||
|
||||
export
|
||||
withPrec : HasEnv m => PPrec -> m a -> m a
|
||||
|
@ -164,9 +164,8 @@ export PrettyHL Name where prettyM = pure . pretty . toDots
|
|||
export
|
||||
prettyStr : PrettyHL a => {default True unicode : Bool} -> a -> String
|
||||
prettyStr {unicode} =
|
||||
renderString .
|
||||
layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) .
|
||||
pretty0 {unicode}
|
||||
let layout = layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) in
|
||||
renderString . layout . pretty0 {unicode}
|
||||
|
||||
|
||||
export
|
||||
|
|
|
@ -37,7 +37,7 @@ DSubst = Subst Dim
|
|||
export %inline
|
||||
prettyDSubst : Pretty.HasEnv m => DSubst from to -> m (Doc HL)
|
||||
prettyDSubst th =
|
||||
prettySubstM prettyM (dnames !ask) DVar
|
||||
prettySubstM prettyM (!ask).dnames DVar
|
||||
!(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
|
||||
|
||||
|
||||
|
|
|
@ -118,4 +118,4 @@ prettySubstM pr names bnd op cl th =
|
|||
||| prints with [square brackets] and the `TVar` highlight for variables
|
||||
export
|
||||
PrettyHL (f to) => PrettyHL (Subst f from to) where
|
||||
prettyM th = prettySubstM prettyM (tnames !ask) TVar "[" "]" th
|
||||
prettyM th = prettySubstM prettyM (!ask).tnames TVar "[" "]" th
|
||||
|
|
|
@ -167,7 +167,7 @@ mutual
|
|||
|
||||
export covering
|
||||
prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
|
||||
prettyTSubst s = prettySubstM prettyM (tnames !ask) TVar "[" "]" s
|
||||
prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
|
||||
|
||||
export covering
|
||||
prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
|
||||
|
|
Loading…
Reference in a new issue