From 6263a02f891cbeb1efa65049ecb86f69c13310b1 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 27 Feb 2025 21:05:04 -0500 Subject: [PATCH] Heading support --- src/SSG/Djot/Block.idr | 103 +++++++++++++++++++++++-- src/SSG/Djot/Lines.idr | 7 ++ src/SSG/Djot/Render.idr | 15 ++++ test/djotToHtml/002-headings/Main.idr | 18 +++++ test/djotToHtml/002-headings/expected | 44 +++++++++++ test/djotToHtml/002-headings/pack.toml | 5 ++ test/djotToHtml/002-headings/run | 6 ++ test/djotToHtml/002-headings/test.dj | 38 +++++++++ test/djotToHtml/002-headings/test.ipkg | 9 +++ todo.org | 16 +++- 10 files changed, 251 insertions(+), 10 deletions(-) create mode 100644 test/djotToHtml/002-headings/Main.idr create mode 100644 test/djotToHtml/002-headings/expected create mode 100644 test/djotToHtml/002-headings/pack.toml create mode 100644 test/djotToHtml/002-headings/run create mode 100644 test/djotToHtml/002-headings/test.dj create mode 100644 test/djotToHtml/002-headings/test.ipkg diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr index d2b0677..64bc98a 100644 --- a/src/SSG/Djot/Block.idr +++ b/src/SSG/Djot/Block.idr @@ -5,6 +5,7 @@ import SSG.Djot.Inline import SSG.Djot.Lines import Control.Eff +import Data.Nat import Data.Maybe import Data.String import Derive.Prelude @@ -20,23 +21,31 @@ import System %hide Generics.Derive.Show %hide Generics.Derive.Eq ---* Data Structures * +--****************************** +--* Data Structures * +--****************************** ||| Types of block level element public export data BlockType : Type where TParagraph : BlockType + THeading : BlockType %runElab derive "BlockType" [Generic, Show, Eq, DecEq] ||| A block element public export data Block : BlockType -> Type where - Paragraph : (content : List (Inline)) -> Block TParagraph + Paragraph : (content : List Inline) -> Block TParagraph + Heading : (level : Nat) -> (content : List Inline) + -> {auto non_zero : IsSucc level} -> {auto in_range : level `LTE` 6} + -> Block THeading %runElab derive "Block" [Show, Eq] ---* Parsing Utilities * +--****************************** +--* Parsing Utilities * +--****************************** ||| Type alias for block parsing BParser : Type -> Type @@ -79,19 +88,78 @@ runBParser : (input : String) -> BParser t -> Maybe t runBParser input x = map fst . extract . runFail . runLines input $ x ---* Syntax * +||| Returns true if a character is horizontal whitespace +isHoriz : Char -> Bool +isHoriz ' ' = True +isHoriz '\t' = True +isHoriz _ = False + +--****************************** +--* Syntax * +--****************************** -- Forward declare for mutual recursion ||| Top level block parser pBlock : BParser (t : BlockType ** Block t) +-- Paragraph + paragraph : BParser (Block TParagraph) paragraph = do contents <- map (inline . joinBy "\n") $ slurp blankLine pure $ Paragraph contents +-- Heading + +record HeadingLevel where + constructor MkHL + level : Nat + {auto non_zero : IsSucc level} + {auto in_range : level `LTE` 6} + +acceptHeadingPrefix : String -> Maybe (HeadingLevel, String) +acceptHeadingPrefix str = + let (level, str) = acceptHeadingPrefix' 0 str + in case isItSucc level of + Yes non_zero => + case level `isLTE` 6 of + Yes in_range => Just $ (MkHL level, str) + No _ => Nothing + No _ => Nothing + where + acceptHeadingPrefix' : (acc : Nat) -> String -> (Nat, String) + acceptHeadingPrefix' acc str with (asList str) + acceptHeadingPrefix' acc "" | [] = (acc, "") + acceptHeadingPrefix' acc (strCons '#' str) | ('#' :: x) = + acceptHeadingPrefix' (S acc) str | x + acceptHeadingPrefix' acc (strCons c str) | (c :: x) = + if isHoriz c + then acceptHeadingPrefix' acc str | x + else (acc, strCons c str) + +headingFirstLine : BParser (HeadingLevel, String) +headingFirstLine = do + first <- take >>= fromJust + fromJust $ acceptHeadingPrefix first + +heading : BParser (Block THeading) +heading = do + (MkHL level {non_zero} {in_range}, first) <- headingFirstLine + rest <- slurp blankLine + let contents = joinBy "\n" $ first :: map (stripPrefix level) rest + pure $ Heading level (inline contents) + where + stripPrefix : (l : Nat) -> String -> String + stripPrefix l str with (asList str) + stripPrefix 0 str | _ = str + stripPrefix (S k) "" | [] = "" + stripPrefix (S k) (strCons '#' str) | ('#' :: x) = stripPrefix k str | x + stripPrefix (S k) (strCons c str) | (c :: x) = strCons c str + -- Definition for top level block parser -pBlock = selectParser paragraph [] +pBlock = selectParser paragraph + [ (isJust . acceptHeadingPrefix, heading) + ] --****************************** @@ -106,7 +174,9 @@ block input = Nothing => (_ ** []) Just x => fromList x ---* Unit Tests * +--****************************** +--* Unit Tests * +--****************************** [myshow] Show (t : BlockType ** Block t) where show (_ ** block) = show block @@ -138,3 +208,24 @@ smokeTwoParagraph = golden "Hello World!\n\nHello Alice!" [Paragraph [Text "Hello World!"], Paragraph [Text "Hello Alice!"]] + +-- @@test Heading Smoke +smokeHeading : IO Bool +smokeHeading = + golden + "# Level 1 Heading" + [Heading 1 [Text "Level 1 Heading"]] + +-- @@test Multiline Prefixed Heading Smoke +smokeHeadingMultilinePrefixed : IO Bool +smokeHeadingMultilinePrefixed = + golden + "# Level 1\n# Heading" + [Heading 1 [Text "Level 1", SoftLineBreak, Text "Heading"]] + +-- @@test Multiline Nonprefixed Heading Smoke +smokeHeadingMultilineNonprefixed : IO Bool +smokeHeadingMultilineNonprefixed = + golden + "# Level 1\nHeading" + [Heading 1 [Text "Level 1", SoftLineBreak, Text "Heading"]] diff --git a/src/SSG/Djot/Lines.idr b/src/SSG/Djot/Lines.idr index 4108762..1dd7a8b 100644 --- a/src/SSG/Djot/Lines.idr +++ b/src/SSG/Djot/Lines.idr @@ -57,6 +57,13 @@ slurp predicate = do | _ => pure [] map (x ::) (slurp predicate) +||| Pop the next line and ignore its value +export +drop : Has Lines fs => Eff fs () +drop = do + _ <- take + pure () + --************************ --* Effect Handlers * --************************ diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index b610349..2e7aebd 100644 --- a/src/SSG/Djot/Render.idr +++ b/src/SSG/Djot/Render.idr @@ -6,6 +6,7 @@ import SSG.Djot.Inline import SSG.Djot.Block import Data.List +import Data.Nat ||| Render a single inline element as HTML export @@ -30,6 +31,20 @@ renderBlocks : {types: _} -> DList _ Block types -> (types' ** DList _ Html type renderBlock (Paragraph content) = (_ ** Normal "p" [] (snd (renderInlines content))) +renderBlock (Heading 1 content {non_zero = ItIsSucc} {in_range}) = + (_ ** Normal "h1" [] (snd (renderInlines content))) +renderBlock (Heading 2 content {non_zero = ItIsSucc} {in_range}) = + (_ ** Normal "h2" [] (snd (renderInlines content))) +renderBlock (Heading 3 content {non_zero = ItIsSucc} {in_range}) = + (_ ** Normal "h3" [] (snd (renderInlines content))) +renderBlock (Heading 4 content {non_zero = ItIsSucc} {in_range}) = + (_ ** Normal "h4" [] (snd (renderInlines content))) +renderBlock (Heading 5 content {non_zero = ItIsSucc} {in_range}) = + (_ ** Normal "h5" [] (snd (renderInlines content))) +renderBlock (Heading 6 content {non_zero = ItIsSucc} {in_range}) = + (_ ** Normal "h6" [] (snd (renderInlines content))) +renderBlock (Heading (6 + (S n)) content {non_zero = ItIsSucc} {in_range}) = + absurd in_range renderBlocks xs = dMap' (\_, x => renderBlock x) xs diff --git a/test/djotToHtml/002-headings/Main.idr b/test/djotToHtml/002-headings/Main.idr new file mode 100644 index 0000000..64b3cdf --- /dev/null +++ b/test/djotToHtml/002-headings/Main.idr @@ -0,0 +1,18 @@ +module Main + +import SSG.Djot +import SSG.HTML + +import System +import System.File + +main : IO () +main = do + Right contents <- readFile "./test.dj" + | Left err => do + printLn err + exitFailure + let (_ ** blocks) = block contents + let html = renderDocument blocks + let output = render html + putStrLn output diff --git a/test/djotToHtml/002-headings/expected b/test/djotToHtml/002-headings/expected new file mode 100644 index 0000000..950af1d --- /dev/null +++ b/test/djotToHtml/002-headings/expected @@ -0,0 +1,44 @@ + + + +

Level 1 Heading

+

Level 2 Heading

+

Level 3 Heading

+

Level 4 Heading

+
Level 5 Heading
+
Level 6 Heading
+

####### Level 7 Not a heading

+

+ Multiline heading + with prefix +

+

+ Multiline heading + with prefix and some extra whitespace +

+

+ Level 2 multiline heading + with prefix +

+

+ Multiline heading + with no prefix +

+

+ Level 2 multiline heading + with no prefix +

+

+ Unprefixed multiline heading + with some indentation +

+

+ Heading level 1 + # With a level 2 right after it (this line shouldn't be a heading) +

+

+ Heading level 2 + With a level 1 right after it (this line shouldn't be a heading) +

+ + diff --git a/test/djotToHtml/002-headings/pack.toml b/test/djotToHtml/002-headings/pack.toml new file mode 100644 index 0000000..d2e5465 --- /dev/null +++ b/test/djotToHtml/002-headings/pack.toml @@ -0,0 +1,5 @@ +[custom.all.SSG] +type = "local" +path = "../../.." +ipkg = "SSG.ipkg" +test = "test/test.ipkg" diff --git a/test/djotToHtml/002-headings/run b/test/djotToHtml/002-headings/run new file mode 100644 index 0000000..6b5ab53 --- /dev/null +++ b/test/djotToHtml/002-headings/run @@ -0,0 +1,6 @@ +rm -rf build/ + +flock "$1" pack -q install-deps test.ipkg +pack -q run test.ipkg + +rm -rf build/ diff --git a/test/djotToHtml/002-headings/test.dj b/test/djotToHtml/002-headings/test.dj new file mode 100644 index 0000000..3f1319e --- /dev/null +++ b/test/djotToHtml/002-headings/test.dj @@ -0,0 +1,38 @@ +# Level 1 Heading + +## Level 2 Heading + +### Level 3 Heading + +#### Level 4 Heading + +##### Level 5 Heading + +###### Level 6 Heading + +####### Level 7 Not a heading + +# Multiline heading +# with prefix + +# Multiline heading +# with prefix and some extra whitespace + +## Level 2 multiline heading +## with prefix + + +# Multiline heading +with no prefix + +## Level 2 multiline heading +with no prefix + +# Unprefixed multiline heading + with some indentation + +# Heading level 1 +## With a level 2 right after it (this line shouldn't be a heading) + +## Heading level 2 +# With a level 1 right after it (this line shouldn't be a heading) diff --git a/test/djotToHtml/002-headings/test.ipkg b/test/djotToHtml/002-headings/test.ipkg new file mode 100644 index 0000000..e727cbf --- /dev/null +++ b/test/djotToHtml/002-headings/test.ipkg @@ -0,0 +1,9 @@ +package a-test + +depends = SSG + , hedgehog + , eff + +main = Main + +executable = test diff --git a/todo.org b/todo.org index cce0eed..df1305b 100644 --- a/todo.org +++ b/todo.org @@ -10,13 +10,12 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Refine =location= in =ParserLocation= ** TODO Error messages ** TODO Combinators for predictive parsing -* Djot [3/38] +* Djot [4/40] :PROPERTIES: :COOKIE_DATA: recursive :END: -** Parsing [3/33] +** Parsing [4/34] *** Block Level -**** TODO Heading **** TODO Block Quote **** TODO List Item **** TODO List @@ -30,6 +29,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Block Attributes **** TODO Heading Links **** DONE Paragraph +**** DONE Heading *** Inline **** TODO Escaped Text **** TODO Link @@ -40,7 +40,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Highlighted **** TODO Super/subscript **** TODO Insert/delete -**** TODO Smart Puncuation +**** TODO Smart Punctuation **** TODO Math **** TODO Footnote Reference **** TODO Comment @@ -52,9 +52,17 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se *** Lines effect **** TODO =IO= Backed implementation *** Known Inaccuracies +**** TODO Stripping of prefixes from multiline headings isn't entirely accurate +Currently, it strips at least =level= ~#~'s from the start of the line, but doesn't check to see if its the correct number of them. +I need to see how other implementations handle this ** Extensions *** TODO GFM-style alerts *** TODO Emoji extension **** TODO Unicode Emoji **** TODO Icon font emoji **** TODO Autolink for source forges +** Misc +*** TODO Add =fromString= for =Inline= +* Features +** TODO Preview rendered post in terminal +Centered headings, text styling, and syntax highlighted code blocks