checkpoint

This commit is contained in:
Nathan McCarty 2025-02-23 17:05:28 -05:00
parent 75a21b8da6
commit 7ef90867f2
10 changed files with 124 additions and 17 deletions

View file

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

View file

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

View file

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

View file

@ -8,17 +8,19 @@
<h5>Level 5 Heading</h5>
<h6>Level 6 Heading</h6>
<p>####### Level 7 Not a Heading</p>
<h1>A heading that spans multiple lines</h1>
<h1>Heading</h1>
<p># A heading that spans multiple lines</p>
<p># Heading</p>
<p>Some content</p>
<h2>A sub heading</h2>
<p>## A sub heading</p>
<p>Even more content</p>
<h1>Back up</h1>
<p># Back up</p>
<p>Some final content</p>
<h1>A Multiline Heading</h1>
<h2>A Level 2 Multiline Heading</h2>
<p>## Heading ### Not a heading</p>
<p>### Heading ## Not a heading</p>
<p>## A Level 2 ## Multiline Heading</p>
<h2>Heading</h2>
<p>### Not a heading</p>
<h3>Heading</h3>
<h2>Not a heading</h2>
<h1>A Multiline Heading</h1>
<h2>A Level 2 Multiline Heading</h2>
<h1>A Multiline Heading</h1>

View file

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

View file

@ -0,0 +1,22 @@
<!DOCTYPE HTML>
<html lang=en>
<body>
<blockquote>
<p>A single line block quote</p>
</blockquote>
<blockquote>
<p>This is a multi-line blockquote With no linebreaks</p>
</blockquote>
<blockquote>
<p>This is a multi-line block quote with</p>
<p>A line break</p>
</blockquote>
<blockquote>
<p>
This is a block quote with a
<br>
hard break in it
</p>
</blockquote>
</body>
</html>

View file

@ -0,0 +1,6 @@
rm -rf build/
flock "$1" pack -q install-deps test.ipkg
pack -q run test.ipkg
rm -rf build/

View file

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

View file

@ -0,0 +1,7 @@
package a-test
depends = SSG
main = Main
executable = test

View file

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