diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr index ecc713d..80d11f1 100644 --- a/src/SSG/Djot/Inline.idr +++ b/src/SSG/Djot/Inline.idr @@ -2,7 +2,7 @@ module SSG.Djot.Inline import Control.Eff -import Data.List.Lazy +import Data.List1 import Data.Maybe import Data.String import Derive.Prelude @@ -21,6 +21,7 @@ import System public export data Inline : Type where Text : (text : String) -> Inline + SoftLineBreak : Inline %runElab derive "Inline" [Eq, Show, Pretty] @@ -30,13 +31,13 @@ data Inline : Type where ||| Type alias for inline parsing IParser : Type -> Type -IParser t = Eff [State (List Char), Choose] t +IParser t = Eff [State (List Char), Fail] t ||| Get the next char, modifiying the state popChar : IParser Char popChar = do x :: xs <- get - | [] => empty + | [] => fail put xs pure x @@ -44,24 +45,32 @@ popChar = do peekChar : IParser Char peekChar = do x :: xs <- get - | [] => empty + | [] => fail pure x ||| Attempt to parse something without propagating the failure try : IParser t -> IParser (Maybe t) try x = do state <- get - x <- lift . runChoose {f = Maybe} $ x + x <- lift . runFail $ x case x of Nothing => do put state pure Nothing Just y => pure $ Just y + ||| Choose a parser oneOf : List (IParser t) -> IParser t -oneOf [] = empty -oneOf (x :: xs) = x `alt` oneOf xs +oneOf [] = fail +oneOf (x :: xs) = do + state <- get + x <- lift . runFail $ x + case x of + Nothing => do + put state + oneOf xs + Just y => pure y ||| Parse 0+ of something many : IParser t -> IParser (List t) @@ -70,10 +79,44 @@ many x = do | _ => pure [] map (y ::) $ many x +||| Parse 1+ of something +atLeastOne : IParser t -> IParser (List1 t) +atLeastOne x = do + Just y <- try x + | _ => fail + map (y :::) (many x) + +||| Match exactly the given string +exactly : String -> IParser (List Char) +exactly str = exactly' (unpack str) + where + exactly' : List Char -> IParser (List Char) + exactly' [] = pure [] + exactly' (x :: xs) = do + y <- popChar + if x == y + then map (x ::) (exactly' xs) + else fail + +||| Match vertical whitespace +vert : IParser (List Char) +vert = oneOf + [ exactly "\n" + , exactly "\r\n" + , exactly "\r" + ] + +||| Match horizontal whitespace +horiz : IParser (List Char) +horiz = oneOf + [ exactly " " + , exactly "\t" + ] + ||| Run a parser runIParser : (str : String) -> IParser t -> Maybe t runIParser str x = - fst . extract . runState (unpack str) . runChoose {f = Maybe} $ x + fst . extract . runState (unpack str) . runFail $ x --****************************** --* Syntax * @@ -89,9 +132,23 @@ text = do c <- popChar pure $ Text (singleton c) +||| Parse a soft linebreak +softLineBreak : IParser Inline +softLineBreak = do + _ <- atLeastOne singleBreak + pure SoftLineBreak + where + singleBreak : IParser () + singleBreak = do + _ <- many horiz + _ <- vert + _ <- many horiz + pure () + -- Definition of pInline pInline = oneOf - [ text + [ softLineBreak + , text ] --****************************** @@ -100,13 +157,22 @@ pInline = oneOf ||| Combine adjacent Text entries combineTexts : List Inline -> List Inline +combineTexts [] = [] combineTexts (Text a :: (Text b :: xs)) = combineTexts (Text (a ++ b) :: xs) -combineTexts xs = xs +combineTexts (x :: xs) = x :: combineTexts xs + +||| Remove trailing soft line breaks +removeTrailingSoftbreak : List Inline -> List Inline +removeTrailingSoftbreak xs = reverse (removeTrailingSoftbreak' (reverse xs)) + where + removeTrailingSoftbreak' : List Inline -> List Inline + removeTrailingSoftbreak' (SoftLineBreak :: xs) = removeTrailingSoftbreak' xs + removeTrailingSoftbreak' xs = xs ||| Top level post processor postProcess : List Inline -> List Inline -postProcess xs = combineTexts xs +postProcess xs = removeTrailingSoftbreak . combineTexts $ xs --****************************** --* Top Level Parsing Function * @@ -137,3 +203,23 @@ golden input reference = do testTextAsText : IO Bool testTextAsText = golden "Hello World!" [Text "Hello World!"] + +-- @@test Soft line break smoke +smokeSoftLineBreak : IO Bool +smokeSoftLineBreak = + golden "Hello\nWorld!" [Text "Hello", SoftLineBreak, Text "World!"] + +-- @@test Soft line break double line break +testDoubleSoftLineBreak : IO Bool +testDoubleSoftLineBreak = + golden "Hello\n\nWorld!" [Text "Hello", SoftLineBreak, Text "World!"] + +-- @@test Soft line break trailing line break +testTrailingSoftLineBreak : IO Bool +testTrailingSoftLineBreak = + golden "Hello\n\nWorld!\n" [Text "Hello", SoftLineBreak, Text "World!"] + +-- @@test Soft line break multiple trailing line breaks +testTrailingSoftLineBreaks : IO Bool +testTrailingSoftLineBreaks = + golden "Hello\n\nWorld!\n\n\n" [Text "Hello", SoftLineBreak, Text "World!"] diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index a2a0092..a6b8b03 100644 --- a/src/SSG/Djot/Render.idr +++ b/src/SSG/Djot/Render.idr @@ -5,16 +5,19 @@ import SSG.HTML import SSG.Djot.Inline import SSG.Djot.Block +import Data.List + ||| Render a single inline element as HTML export -renderInline : Inline -> (t ** Html t) +renderInline : Inline -> Maybe (t ** Html t) -- FIXME: escape text -renderInline (Text text) = (_ ** Text text) +renderInline (Text text) = Just (_ ** Text text) +renderInline SoftLineBreak = Nothing ||| Render a list of inline elments to html export renderInlines : List Inline -> (types ** DList _ Html types) -renderInlines xs = fromList $ map renderInline xs +renderInlines xs = fromList . catMaybes $ map renderInline xs ||| Render a single block element as HTML export diff --git a/test/djotToHtml/001-paragraph/expected b/test/djotToHtml/001-paragraph/expected index d83d19b..6875061 100644 --- a/test/djotToHtml/001-paragraph/expected +++ b/test/djotToHtml/001-paragraph/expected @@ -3,10 +3,14 @@

Hello World!

Hello Alice!

-

A Multi-line -Paragraph

+

+ A Multi-line + Paragraph +

Two line breaks

-

A multiline paragraph - with some indentation

+

+ A multiline paragraph + with some indentation +