Soft line break support

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!"]

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

test/djotToHtml/001-paragraph/expected

@@ -3,10 +3,14 @@
   <body>
     <p>Hello World!</p>
     <p>Hello Alice!</p>
-    <p>A Multi-line
-Paragraph</p>
+    <p>
+      A Multi-line
+      Paragraph
+    </p>
     <p>Two line breaks</p>
-    <p>A multiline paragraph
-  with some indentation</p>
+    <p>
+      A multiline paragraph
+      with some indentation
+    </p>
   </body>
 </html>