Idris/ssg
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Pretty print internal representation in Djot utility

Browse source
This commit is contained in:
Nathan McCarty 2025-02-21 16:34:41 -05:00
parent 68928aeb20
commit f54df1d2a4
4 changed files with 15 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/SSG/Djot/Block.idr
View file

@ -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 *

3
src/SSG/Djot/Inline.idr
View file

@ -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 *