From 2446655b0861f196452afeec6d504398b5ccc1ab Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 11 Apr 2022 21:58:33 +0200 Subject: [PATCH] move BannerOpts to PrettyOpts --- src/Quox.idr | 23 +++++++---------------- src/Quox/Pretty.idr | 32 +++++++++++++++++++++++--------- 2 files changed, 30 insertions(+), 25 deletions(-) diff --git a/src/Quox.idr b/src/Quox.idr index 2b4c6d3..56cfbc3 100644 --- a/src/Quox.idr +++ b/src/Quox.idr @@ -12,17 +12,8 @@ import Data.Vect import Control.ANSI -public export -record BannerOpts where - constructor MakeBannerOpts - unicode, color : Bool - -public export -defBannerOpts : BannerOpts -defBannerOpts = MakeBannerOpts {unicode = True, color = True} - private -text : BannerOpts -> List String +text : PrettyOpts -> List String text _ = ["", #" ___ ___ _____ __ __"#, @@ -32,7 +23,7 @@ text _ = ""] private -qtuwu : BannerOpts -> List String +qtuwu : PrettyOpts -> List String qtuwu opts = if opts.unicode then [#" ___,-´⎠ "#, @@ -50,7 +41,7 @@ qtuwu opts = #" (---) | "#] private -join1 : BannerOpts -> String -> String -> String +join1 : PrettyOpts -> String -> String -> String join1 opts l r = if opts.color then " " <+> show (colored Green l) <+> " " <+> show (colored Magenta r) @@ -58,7 +49,7 @@ join1 opts l r = " " <+> l <+> " " <+> r export -banner : BannerOpts -> String +banner : PrettyOpts -> String banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts) export @@ -70,6 +61,6 @@ tm = main : IO Unit main = do - putStrLn $ banner defBannerOpts - prettyTerm tm - prettyTerm $ pushSubstsT tm + putStrLn $ banner defPrettyOpts + prettyTermDef tm + prettyTermDef $ pushSubstsT tm diff --git a/src/Quox/Pretty.idr b/src/Quox/Pretty.idr index e7e2e26..776f0da 100644 --- a/src/Quox/Pretty.idr +++ b/src/Quox/Pretty.idr @@ -14,6 +14,16 @@ import public Control.Monad.Reader %default total +public export +record PrettyOpts where + constructor MakePrettyOpts + unicode, color : Bool + +public export +defPrettyOpts : PrettyOpts +defPrettyOpts = MakePrettyOpts {unicode = True, color = True} + + public export data HL = Delim @@ -160,8 +170,8 @@ pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL) pretty0M = local {prec := Outer} . prettyM export %inline -pretty0 : PrettyHL a => {default True unicode : Bool} -> a -> Doc HL -pretty0 x {unicode} = +pretty0 : PrettyHL a => (unicode : Bool) -> a -> Doc HL +pretty0 unicode x = let env = MakePrettyEnv {dnames = [], tnames = [], unicode, prec = Outer} in runReader env $ prettyM x @@ -180,10 +190,10 @@ export PrettyHL Name where prettyM = pure . pretty . toDots export %inline -prettyStr : PrettyHL a => {default True unicode : Bool} -> a -> String -prettyStr {unicode} = +prettyStr : PrettyHL a => (unicode : Bool) -> a -> String +prettyStr unicode = let layout = layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) in - renderString . layout . pretty0 {unicode} + renderString . layout . pretty0 unicode export @@ -199,10 +209,14 @@ termHL Free = color BrightWhite termHL Syntax = color BrightCyan export %inline -prettyTerm : {default True color, unicode : Bool} -> PrettyHL a => a -> IO Unit -prettyTerm x {color, unicode} = - let reann = if color then map termHL else unAnnotate in - Terminal.putDoc $ reann $ pretty0 x {unicode} +prettyTerm : PrettyOpts -> PrettyHL a => a -> IO Unit +prettyTerm opts x = + let reann = if opts.color then map termHL else unAnnotate in + Terminal.putDoc $ reann $ pretty0 opts.unicode x + +export %inline +prettyTermDef : PrettyHL a => a -> IO Unit +prettyTermDef = prettyTerm defPrettyOpts infixr 6