From 7ef90867f25697c704c37ddab6b7261cc162d873 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 23 Feb 2025 17:05:28 -0500 Subject: [PATCH] checkpoint --- src/SSG/Djot/Block.idr | 50 ++++++++++++++++++--- src/SSG/Djot/Common.idr | 7 +-- src/SSG/Djot/Render.idr | 3 ++ test/djot-to-html/003-headings/expected | 16 ++++--- test/djot-to-html/004-blockquotes/Main.idr | 16 +++++++ test/djot-to-html/004-blockquotes/expected | 22 +++++++++ test/djot-to-html/004-blockquotes/run | 6 +++ test/djot-to-html/004-blockquotes/test.dj | 11 +++++ test/djot-to-html/004-blockquotes/test.ipkg | 7 +++ todo.org | 3 +- 10 files changed, 124 insertions(+), 17 deletions(-) create mode 100644 test/djot-to-html/004-blockquotes/Main.idr create mode 100644 test/djot-to-html/004-blockquotes/expected create mode 100644 test/djot-to-html/004-blockquotes/run create mode 100644 test/djot-to-html/004-blockquotes/test.dj create mode 100644 test/djot-to-html/004-blockquotes/test.ipkg diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr index 273f481..e9754d7 100644 --- a/src/SSG/Djot/Block.idr +++ b/src/SSG/Djot/Block.idr @@ -17,6 +17,7 @@ import Derive.Pretty -- For iutils unit tests import System +import Debug.Trace %language ElabReflection @@ -63,6 +64,7 @@ public export data Block : Type where Paragraph : (contents : List1 Inline) -> Block Heading : (level : HeaderLevel) -> (contents : List1 Inline) -> Block + BlockQuote : (contents : List1 Block) -> Block %runElab derive "List1" [Pretty] %runElab derive "Block" [Show, Eq, Pretty] @@ -75,7 +77,7 @@ data Block : Type where prefixedLine : (pfx : PS b) -> PS String prefixedLine pfx = do _ <- pfx - cs <- nonBlankLine + cs <- line pure $ pack cs -- Parses a block prefixed by the given character string with the given parser @@ -89,6 +91,14 @@ parsePrefixedBlock pfx parser = do --* Syntax * --***************** +-- Forward declare our top level parsers, so we can get mutually recursive + +export +block : PS Block + +export +blocks : PS (List Block) + --------------- -- Paragraph -- --------------- @@ -138,25 +148,44 @@ heading = do load state inlines <- parsePrefixedBlock (headingPrefix (length levelMarker)) inline -- djot demands a blank line or the end of file after a heading - _ <- blankLineOrEnd + _ <- many blankLine pure $ Heading level inlines +---------------- +-- Blockquote -- +---------------- + +blockquote : PS Block +blockquote = do + blocks <- parsePrefixedBlock (oneOfE "" [prefixedEmpty, thisString "> "]) blocks + case blocks of + [] => throw "Empty block quote" + (x :: xs) => pure $ BlockQuote (x ::: xs) + where + prefixedEmpty : PS String + prefixedEmpty = do + _ <- thisString ">" + -- peek the rest of the line, make sure it's empty + state <- save + cs <- many nonTerminal + load state + if all isHorizontalWhitespace cs + then pure ">" + else throw "Invalid blockquote line" + -------------------------- -- Overall Block Parser -- -------------------------- -export -block : PS Block block = do -- eat up any blank lines _ <- many blankLine oneOfE "" [ heading + , blockquote , paragraph ] -export -blocks : PS (List Block) blocks = many block --***************** @@ -219,3 +248,12 @@ blockMultilineUnprefixed = Heading 1 (Text "Level 1" ::: [SoftLineBreak, Text "More text"]) ] in golden input ref blocks + +-- @@test Single Line Blockquote +blockSingleLineBlockquote : IO Bool +blockSingleLineBlockquote = + let input = "> Blockquote" + ref = [ + BlockQuote ( Paragraph (inlineFromString' "Blockquote") ::: []) + ] + in golden input ref blocks diff --git a/src/SSG/Djot/Common.idr b/src/SSG/Djot/Common.idr index 8f8b71b..0f35892 100644 --- a/src/SSG/Djot/Common.idr +++ b/src/SSG/Djot/Common.idr @@ -92,8 +92,10 @@ terminal = do export line : PS (List Char) line = do + False <- parseEoF + | True => throw "Already at EoF" cs <- many nonTerminal - _ <- lineEnding + terminal pure cs export @@ -111,8 +113,7 @@ blankLine = do export nonBlankLine : PS (List Char) nonBlankLine = do - cs <- many nonTerminal - _ <- terminal + cs <- line case all isHorizontalWhitespace cs of True => throw "blank line" False => pure cs diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index b218f6b..e88f984 100644 --- a/src/SSG/Djot/Render.idr +++ b/src/SSG/Djot/Render.idr @@ -64,6 +64,9 @@ renderBlock (Heading level contents) = let (_ ** xs) = renderInlines $ forget contents (level ** _ ) = headingLevel level in (_ ** Normal level [] xs) +renderBlock (BlockQuote contents) = + let (_ ** contents) = fromList . map renderBlock . forget $ contents + in (_ ** Normal "blockquote" [] contents) export renderBlocks : List Block -> (types : List String ** DList _ Html types) diff --git a/test/djot-to-html/003-headings/expected b/test/djot-to-html/003-headings/expected index 91f7ee8..ae84cb0 100644 --- a/test/djot-to-html/003-headings/expected +++ b/test/djot-to-html/003-headings/expected @@ -8,17 +8,19 @@
Level 5 Heading
Level 6 Heading

####### Level 7 Not a Heading

-

A heading that spans multiple lines

-

Heading

+

# A heading that spans multiple lines

+

# Heading

Some content

-

A sub heading

+

## A sub heading

Even more content

-

Back up

+

# Back up

Some final content

A Multiline Heading

-

A Level 2 Multiline Heading

-

## Heading ### Not a heading

-

### Heading ## Not a heading

+

## A Level 2 ## Multiline Heading

+

Heading

+

### Not a heading

+

Heading

+

Not a heading

A Multiline Heading

A Level 2 Multiline Heading

A Multiline Heading

diff --git a/test/djot-to-html/004-blockquotes/Main.idr b/test/djot-to-html/004-blockquotes/Main.idr new file mode 100644 index 0000000..97d8771 --- /dev/null +++ b/test/djot-to-html/004-blockquotes/Main.idr @@ -0,0 +1,16 @@ +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 parsed = djot contents + putStr . render . renderHtml $ parsed diff --git a/test/djot-to-html/004-blockquotes/expected b/test/djot-to-html/004-blockquotes/expected new file mode 100644 index 0000000..1efa208 --- /dev/null +++ b/test/djot-to-html/004-blockquotes/expected @@ -0,0 +1,22 @@ + + + +
+

A single line block quote

+
+
+

This is a multi-line blockquote With no linebreaks

+
+
+

This is a multi-line block quote with

+

A line break

+
+
+

+ This is a block quote with a +
+ hard break in it +

+
+ + \ No newline at end of file diff --git a/test/djot-to-html/004-blockquotes/run b/test/djot-to-html/004-blockquotes/run new file mode 100644 index 0000000..6b5ab53 --- /dev/null +++ b/test/djot-to-html/004-blockquotes/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/djot-to-html/004-blockquotes/test.dj b/test/djot-to-html/004-blockquotes/test.dj new file mode 100644 index 0000000..69790d6 --- /dev/null +++ b/test/djot-to-html/004-blockquotes/test.dj @@ -0,0 +1,11 @@ +> A single line block quote + +> This is a multi-line blockquote +> With no linebreaks + +> This is a multi-line block quote with +> +> A line break + +> This is a block quote with a \ +> hard break in it diff --git a/test/djot-to-html/004-blockquotes/test.ipkg b/test/djot-to-html/004-blockquotes/test.ipkg new file mode 100644 index 0000000..0efef9e --- /dev/null +++ b/test/djot-to-html/004-blockquotes/test.ipkg @@ -0,0 +1,7 @@ +package a-test + +depends = SSG + +main = Main + +executable = test diff --git a/todo.org b/todo.org index d263555..7f89a0d 100644 --- a/todo.org +++ b/todo.org @@ -9,7 +9,7 @@ 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 [7/43] +* Djot [7/44] :PROPERTIES: :COOKIE_DATA: recursive :END: @@ -55,6 +55,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Support all types of whitespace *** TODO Escaping *** TODO Whitespace class +** TODO Lazy indentation ** TODO hex escapes ** TODO GFM style alerts ** TODO Group adjacent =Text=s into a =String=