add runPrettyWith, etc

lib/Quox/Pretty.idr

@@ -175,14 +175,26 @@ pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL)
 pretty0M = local {prec := Outer} . prettyM
 
 export %inline
-runPretty : (unicode : Bool) -> Reader PrettyEnv a -> a
+runPrettyWith : (unicode : Bool) -> (dnames, tnames : SnocList BaseName) ->
-runPretty unicode act =
+                Reader PrettyEnv a -> a
-  let env = MakePrettyEnv {dnames = [<], tnames = [<], unicode, prec = Outer} in
+runPrettyWith unicode dnames tnames act =
+  let env = MakePrettyEnv {dnames, tnames, unicode, prec = Outer} in
   runReader env act
 
+export %inline
+runPretty : (unicode : Bool) -> Reader PrettyEnv a -> a
+runPretty unicode = runPrettyWith unicode [<] [<]
+
+export %inline
+pretty0With : PrettyHL a => (unicode : Bool) ->
+             (dnames, tnames : SnocList BaseName) ->
+             a -> Doc HL
+pretty0With {unicode, dnames, tnames} =
+  runPrettyWith {unicode, dnames, tnames} . prettyM
+
 export %inline
 pretty0 : PrettyHL a => (unicode : Bool) -> a -> Doc HL
-pretty0 unicode = runPretty unicode . prettyM
+pretty0 unicode = pretty0With unicode [<] [<]
 
 
 export

lib/Quox/Syntax/Term/Pretty.idr

@@ -271,9 +271,4 @@ prettyTerm : IsQty q => PrettyHL q => (unicode : Bool) ->
              (dnames : NContext d) -> (tnames : NContext n) ->
              Term q d n -> Doc HL
 prettyTerm unicode dnames tnames term =
-  let env = MakePrettyEnv {
+  pretty0With unicode (toSnocList' dnames) (toSnocList' tnames) term
-    dnames = toSnocList' dnames,
-    tnames = toSnocList' tnames,
-    unicode, prec = Outer
-  } in
-  runReader env $ prettyM term