From bc1aa21f09109807aa43f50946959a0dd034a6e6 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 3 Sep 2021 16:31:53 +0200
Subject: [PATCH] use dots for record fields

---
 src/Quox/Pretty.idr       | 9 ++++-----
 src/Quox/Syntax/Dim.idr   | 2 +-
 src/Quox/Syntax/Subst.idr | 2 +-
 src/Quox/Syntax/Term.idr  | 2 +-
 4 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/Quox/Pretty.idr b/src/Quox/Pretty.idr
index e44d334..8049a5b 100644
--- a/src/Quox/Pretty.idr
+++ b/src/Quox/Pretty.idr
@@ -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
diff --git a/src/Quox/Syntax/Dim.idr b/src/Quox/Syntax/Dim.idr
index cba8b2e..e445b2e 100644
--- a/src/Quox/Syntax/Dim.idr
+++ b/src/Quox/Syntax/Dim.idr
@@ -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
 
 
diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index 497d6cc..4287a07 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -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
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 8a6ab99..9247619 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -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)