From d6985cad55c8fa51b4434168a5c9697d51b31f7e Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 20 Oct 2023 04:53:49 +0200
Subject: [PATCH] tweak the pretty printer stuff slightly

---
 .../PrettyPrint/Bernardy/Core/Decorate.idr    | 26 +++++++++++++------
 1 file changed, 18 insertions(+), 8 deletions(-)

diff --git a/lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr b/lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr
index c986889..6e73cc6 100644
--- a/lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr
+++ b/lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr
@@ -1,29 +1,37 @@
 -- this module has to be called this because a module A.B's private elements are
 -- still visible to A.B.C, even if they're in different packages. which i don't
 -- think is a good idea but i also don't want to fork prettier over it
+--
+-- also i adapted this code from stefan höck's prettier-ansi package
+-- (https://github.com/idris-community/idris2-ansi)
 module Text.PrettyPrint.Bernardy.Core.Decorate
 
 import public Text.PrettyPrint.Bernardy.Core
 import Data.DPair
 import Data.String
+import Derive.Prelude
+
+%language ElabReflection
 
 
 public export
 record Highlight where
   constructor MkHighlight
   before, after : String
+%name Highlight h
+%runElab derive "Highlight" [Eq]
 
 export
-emptyHL : Highlight -> Bool
-emptyHL (MkHighlight before after) = before == "" && after == ""
+emptyHL : Highlight
+emptyHL = MkHighlight "" ""
 
 
--- taken from prettier-ansi
+-- lifted from prettier-ansi
 private
 decorateImpl : Highlight ->
                (ss : SnocList String) -> (0 _ : NonEmptySnoc ss) =>
                Subset (SnocList String) NonEmptySnoc
-decorateImpl h [<x]      = Element [< h.before ++ x ++ h.after] %search
+decorateImpl h [< x]     = Element [< h.before ++ x ++ h.after] %search
 decorateImpl h (sx :< x) = Element (go [] sx :< (x ++ h.after)) %search
   where
     go : List String -> SnocList String -> SnocList String
@@ -35,17 +43,19 @@ decorateImpl h (sx :< x) = Element (go [] sx :< (x ++ h.after)) %search
 ||| changing its stats like width or height.
 export
 decorateLayout : Highlight -> Layout -> Layout
-decorateLayout h l@(MkLayout content stats) =
-  if emptyHL h then l else
+decorateLayout h (MkLayout content stats) =
   layout (decorateImpl h content) stats
 
 ||| Decorate a `Doc` with the given highlighting *without*
 ||| changing its stats like width or height.
 export
-decorate : {opts : _} -> Highlight -> Doc opts -> Doc opts
-decorate h doc = doc >>= \l => pure (decorateLayout h l)
+decorate : {opts : LayoutOpts} -> Highlight -> Doc opts -> Doc opts
+decorate h doc =
+  if h == emptyHL then doc else doc >>= pure . decorateLayout h
 
 
+-- this function has nothing to do with highlighting but it's here because it
+-- _also_ needs access to the private stuff
 ||| render a doc with no line breaks at all
 export
 renderInfinite : Doc opts -> String