From f54df1d2a457fe58b84f17c76d11f91997e8bd87 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 21 Feb 2025 16:34:41 -0500
Subject: [PATCH] Pretty print internal representation in Djot utility

---
 SSG.ipkg                | 2 ++
 bin/src/Djot.idr        | 8 +++++++-
 src/SSG/Djot/Block.idr  | 6 ++++--
 src/SSG/Djot/Inline.idr | 3 ++-
 4 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/SSG.ipkg b/SSG.ipkg
index 1df6058..ec92d59 100644
--- a/SSG.ipkg
+++ b/SSG.ipkg
@@ -18,6 +18,8 @@ depends = structures
         , eff
         , refined
         , elab-util
+        , elab-pretty
+        , prettier
 
 -- modules to install
 modules = SSG.Parser.Core
diff --git a/bin/src/Djot.idr b/bin/src/Djot.idr
index 3bdfc57..85a0767 100644
--- a/bin/src/Djot.idr
+++ b/bin/src/Djot.idr
@@ -6,6 +6,8 @@ import System.File
 import SSG.Djot
 import SSG.HTML
 
+import Text.PrettyPrint.Bernardy
+
 main : IO ()
 main = do
   args <- getArgs
@@ -14,8 +16,12 @@ main = do
       Right contents <- readFile file
         | Left err => printLn err
       let parsed = djot contents
-      printLn parsed
       putStr . render $ renderHtml parsed
+    [_, "raw", file] => do
+      Right contents <- readFile file
+        | Left err => printLn err
+      let parsed = djot contents
+      putStrLn . Doc.render (Opts 80) $ pretty parsed
     _ => do
       putStrLn "?"
       exitFailure
diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr
index 14cdbed..067feb0 100644
--- a/src/SSG/Djot/Block.idr
+++ b/src/SSG/Djot/Block.idr
@@ -13,6 +13,7 @@ import Data.String
 
 import Control.Eff
 import Derive.Prelude
+import Derive.Pretty
 
 -- For iutils unit tests
 import System
@@ -32,7 +33,7 @@ data HeaderLevel : Type where
   H5 : HeaderLevel
   H6 : HeaderLevel
 
-%runElab derive "HeaderLevel" [Eq]
+%runElab derive "HeaderLevel" [Eq, Pretty]
 
 export
 Show HeaderLevel where
@@ -63,7 +64,8 @@ data Block : Type where
   Paragraph : (contents : List1 Inline) -> Block
   Heading : (level : HeaderLevel) -> (contents : List1 Inline) -> Block
 
-%runElab derive "Block" [Show, Eq]
+%runElab derive "List1" [Pretty]
+%runElab derive "Block" [Show, Eq, Pretty]
 
 --**************
 --*   Syntax   *
diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr
index 824221a..f5db77f 100644
--- a/src/SSG/Djot/Inline.idr
+++ b/src/SSG/Djot/Inline.idr
@@ -8,6 +8,7 @@ import SSG.Djot.Common
 import Control.Eff
 import Control.Monad.Eval
 import Derive.Prelude
+import Derive.Pretty
 
 -- For iutils unit tests
 import System
@@ -25,7 +26,7 @@ data Inline : Type where
   NonBreakingSpace : Inline
   Text : (c : String) -> Inline
 
-%runElab derive "Inline" [Show, Eq]
+%runElab derive "Inline" [Show, Eq, Pretty]
 
 --******************
 --* PostProcessing *