.gitignore

@@ -1,4 +1,2 @@
 build/
 *.*~
-test/failures
-test/*/*/output

SSG.ipkg

@@ -13,23 +13,14 @@ authors = "Nathan McCarty"
 -- langversion
 
 -- packages to add to search path
-depends = contrib
+depends = structures
-        , structures
-        , tailrec
         , eff
-        , elab-util
-        , elab-pretty
-        , sop
-        , prettier
 
 -- modules to install
-modules = SSG.HTML
+modules = SSG.Parser.Core
+        , SSG.Parser.Markdown
+        , SSG.HTML
         , SSG.HTML.ElementTypes
-        , SSG.Djot
-        , SSG.Djot.Lines
-        , SSG.Djot.Block
-        , SSG.Djot.Inline
-        , SSG.Djot.Render
 
 -- main file (i.e. file to load at REPL)
 main = Main

examples/src/HelloWorld.idr

@@ -5,15 +5,15 @@ import SSG.HTML
 import Structures.Dependent.DList
 
 helloWorld : Html "html"
--- helloWorld =
+helloWorld =
---   tag "html" ["lang" =$ "en"] [] [
+  tag "html" ["lang" =$ "en"] [
---     tag "head" [] [
+    tag "head" [] [
---       tag "title" [] "Example"
+      tag "title" [] "Example"
---     ],
+    ],
---     tag "body" [] [
+    tag "body" [] [
---       tag "p" [] [Text "Hello World!"]
+      tag "p" [] [Text "Hello World!"]
---     ]
+    ]
---   ]
+  ]
 
 main : IO ()
 main = putStr $ render helloWorld

pack.toml

@@ -4,11 +4,6 @@ path = "."
 ipkg = "SSG.ipkg"
 test = "test/test.ipkg"
 
-[custom.all.Djot]
-type = "local"
-path = "."
-ipkg = "Djot.ipkg"
-
 [custom.all.SSG-test]
 type = "local"
 path = "test"

src/SSG/Djot.idr

@@ -1,5 +0,0 @@
-module SSG.Djot
-
-import public SSG.Djot.Inline
-import public SSG.Djot.Block
-import public SSG.Djot.Render

src/SSG/Djot/Block.idr

@@ -1,231 +0,0 @@
-||| DJot Block formatting parser
-module SSG.Djot.Block
-
-import SSG.Djot.Inline
-import SSG.Djot.Lines
-
-import Control.Eff
-import Data.Nat
-import Data.Maybe
-import Data.String
-import Derive.Prelude
-import Derive.Pretty
-import Generics.Derive
-import Structures.Dependent.DList
-
--- Just for iutils unit tests
-import System
-
-%language ElabReflection
-%hide Generics.SOP.values
-%hide Generics.Derive.Show
-%hide Generics.Derive.Eq
-
---******************************
---*       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
-  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     *
---******************************
-
-||| Type alias for block parsing
-BParser : Type -> Type
-BParser t = Eff [Lines, Fail] t
-
--- FIXME: Proper whitespace handling
-||| Detect if a line is blank
-blankLine : String -> Bool
-blankLine = null . trim
-
-||| Select and apply the first matching parser from a list, with a fallback parser
-selectParser :
-  {fallback_type : BlockType} -> {values : _}
-  -> (fallback : BParser (Block fallback_type))
-  -> DList BlockType (\t => (String -> Bool, BParser (Block t))) values
-  -> BParser (t : BlockType ** Block t)
-selectParser fallback [] = do
-  x <- fallback
-  pure (_ ** x)
-selectParser fallback ((pred, parser) :: rest) = do
-  Just line <- peek
-    | _ => fail
-  if pred line
-    then do
-      x <- parser
-      pure (_ ** x)
-    else selectParser fallback rest
-
-||| Repeat a parser until failure or if we are out of lines
-repeat : BParser t -> BParser (List t)
-repeat x = do
-  Just _ <- peek
-    | _ => pure []
-  Just res <- lift . runFail $ x
-    | _ => pure []
-  map (res ::) (repeat x)
-
-||| Run a parser
-runBParser : (input : String) -> BParser t -> Maybe t
-runBParser input x =
-  map fst . extract . runFail . runLines input $ x
-
-||| 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
-  [ (isJust . acceptHeadingPrefix, heading)
-  ]
-
-
---******************************
---* Top Level Parsing Function *
---******************************
-
-||| Parse a string as a sequences of blocks
-export
-block : (input : String) -> (values ** DList BlockType Block values)
-block input =
-  case runBParser input (repeat pBlock) of
-    Nothing => (_ ** [])
-    Just x => fromList x
-
---******************************
---*         Unit Tests         *
---******************************
-
-[myshow] Show (t : BlockType ** Block t) where
-  show (_ ** block) = show block
-
-{values : _} -> Show (DList BlockType Block values) where
-  show xs =
-    let xs = map (show @{myshow}) $ toList xs
-    in "[\{joinBy ", " xs}]"
-
-golden : {values : _}
-  -> (input : String) -> (ref : DList BlockType Block values) -> IO Bool
-golden input ref = do
-  putStrLn "Input: \{show input}"
-  putStrLn "Reference:\n  \{show ref}"
-  let (types ** output) = block input
-  putStrLn "Output:\n  \{show output}"
-  pure $ ref $== output
-
--- @@test Paragraph Smoke
-smokeParagraph : IO Bool
-smokeParagraph =
-  golden
-    "Hello World!"
-    [Paragraph [Text "Hello World!"]]
-
--- @@test Two Paragraph Smoke
-smokeTwoParagraph : IO Bool
-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"]]

src/SSG/Djot/Inline.idr

@@ -1,240 +0,0 @@
-||| Djot inline formatting parser
-module SSG.Djot.Inline
-
-import Control.Eff
-import Data.List1
-import Data.Maybe
-import Data.String
-import Derive.Prelude
-import Derive.Pretty
-
--- Just for iutils unit tests
-import System
-
-%language ElabReflection
-
---******************************
---*       Data Structures      *
---******************************
-
-||| Types of inline styling
-public export
-data Inline : Type where
-  Text : (text : String) -> Inline
-  SoftLineBreak : Inline
-  HardLineBreak : Inline
-
-%runElab derive "Inline" [Eq, Show, Pretty]
-
---******************************
---*      Parsing Utilities     *
---******************************
-
-||| Type alias for inline parsing
-IParser : Type -> Type
-IParser t = Eff [State (List Char), Fail] t
-
-||| Get the next char, modifiying the state
-popChar : IParser Char
-popChar = do
-  x :: xs <- get
-    | [] => fail
-  put xs
-  pure x
-
-||| Get the next char, without modifying the state
-peekChar : IParser Char
-peekChar = do
-  x :: xs <- get
-    | [] => fail
-  pure x
-
-||| Attempt to parse something without propagating the failure
-try : IParser t -> IParser (Maybe t)
-try x = do
-  state <- get
-  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 [] = 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)
-many x = do
-  Just y <- try x
-    | _ => 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) . runFail $ x
-
---******************************
---*           Syntax           *
---******************************
-
--- Forward declare so we can get mutually recursive
-||| Top level parser function for Inline Content
-pInline : IParser Inline
-
-||| Parse a character as plain text
-text : IParser Inline
-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 ()
-
-hardLineBreak : IParser Inline
-hardLineBreak = do
-  _ <- exactly "\\"
-  _ <- many horiz
-  _ <- vert
-  _ <- many horiz
-  pure HardLineBreak
-
--- Definition of pInline
-pInline = oneOf
-  [ hardLineBreak
-  , softLineBreak
-  , text
-  ]
-
---******************************
---*       Post Processing      *
---******************************
-
-||| Combine adjacent Text entries
-combineTexts : List Inline -> List Inline
-combineTexts [] = []
-combineTexts (Text a :: (Text b :: xs)) =
-  combineTexts (Text (a ++ b) :: 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 = removeTrailingSoftbreak . combineTexts $ xs
-
---******************************
---* Top Level Parsing Function *
---******************************
-
-||| Parse a string as inline content
-export
-inline : (input : String) -> List Inline
-inline input =
-  postProcess . fromMaybe [] . runIParser input $ many pInline
-
---******************************
---*         Unit Tests         *
---******************************
-
-golden : (input : String) -> (reference : List Inline) -> IO Bool
-golden input reference = do
-  putStrLn "Input: \{show input}"
-  let opts = Opts 78
-  let ref_pretty = Doc.render opts $ pretty reference
-  putStrLn "Reference:\n\{unlines . map ("  " ++) . lines $ ref_pretty}"
-  let output = inline input
-  let out_pretty = Doc.render opts $ pretty output
-  putStrLn "Output:\n\{unlines . map ("  " ++) . lines $ out_pretty}"
-  pure $ reference == output
-
--- @@test Just text parses as text
-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!"]
-
--- @@test Hard line break smoke
-smokeHardLineBreak : IO Bool
-smokeHardLineBreak =
-  golden "Hello\\\nWorld!" [Text "Hello", HardLineBreak, Text "World!"]

src/SSG/Djot/Lines.idr

@@ -1,135 +0,0 @@
-||| An effect for reading an input as a list of lines
-module SSG.Djot.Lines
-
-import Data.String
-
-import Control.Eff
-
--- Only for iutils unit tests
-import System
-
---************************
---*   Effect Definition  *
---************************
-
-export
-data Lines : Type -> Type where
-  ||| Peek the next line
-  Peek : Lines (Maybe String)
-  ||| Take the next line
-  Take : Lines (Maybe String)
-
---************************
---*    Effect Actions    *
---************************
-
-export
-peek : Has Lines fs => Eff fs (Maybe String)
-peek = send Peek
-
-export
-take : Has Lines fs => Eff fs (Maybe String)
-take = send Take
-
---************************
---* Extra Effect Actions *
---************************
-
-||| Take lines until a line matching the given predicate is encountered, dropping the
-||| all of the matching lines until the first non matching one
-|||
-||| Intended to be used to slurp up to the next blank line, discarding the blanks
-export
-slurp : Has Lines fs => (predicate : String -> Bool) -> Eff fs (List String)
-slurp predicate = do
-  Just line <- peek
-    | _ => pure []
-  if predicate line
-    then do
-      _ <- take
-      Just next <- peek
-        | _ => pure []
-      if predicate next
-        then slurp predicate
-        else pure []
-    else do
-      Just x <- take
-        | _ => 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   *
---************************
-
-||| Split the next line from a string
-nextLine : String -> Maybe (String, String)
-nextLine str =
-  if null str
-    then Nothing
-    else
-      let 
-        (before, after) = break (\c => any (== c) ['\r', '\n']) str
-      in Just (before, removeNewline after)
-  where
-    -- If `after` is empty, we have hit the end of the string, and there is no newline
-    -- character to remove. If it has contents, then we need to remove the newline
-    removeNewline : String -> String
-    removeNewline str with (strM str)
-      removeNewline "" | StrNil = ""
-      removeNewline (strCons '\n' xs) | (StrCons '\n' xs) = xs
-      -- Handle either a \r or a \r\n
-      removeNewline (strCons '\r' xs) | (StrCons '\r' xs) with (strM xs)
-        removeNewline (strCons '\r' "") | (StrCons '\r' "") | StrNil = ""
-        removeNewline (strCons '\r' _) | (StrCons '\r' _) | (StrCons '\n' xs1) = xs1
-        removeNewline (strCons '\r' _) | (StrCons '\r' _) | (StrCons x xs1) = strCons x xs1
-      -- We shouldn't ever hit this case, as we would have to have contents after the
-      -- break, but no newline character, but we fill it in for the sake of totality
-      removeNewline (strCons x xs) | (StrCons x xs) = str
-
-unLines : String -> Lines s -> (s, String)
-unLines str Peek =
-  case nextLine str of
-    Nothing => (Nothing, str)
-    Just (before, after) => (Just before, str)
-unLines str Take =
-  case nextLine str of
-    Nothing => (Nothing, str)
-    Just (before, after) => (Just before, after)
-
-||| Feed a `Lines` from a provided input string
-export
-runLines : Has Lines fs =>
-  (input : String) -> Eff fs t -> Eff (fs - Lines) (t, String)
-runLines input =
-  handleRelayS input (\x, y => pure (y, x)) $ \input2, lns, f =>
-    let (vv, input3) = unLines input2 lns
-    in f input3 vv
-
---************************
---*      Unit Tests      *
---************************
-
--- @@test runLines Smoke Test
-runLinesSmoke : IO Bool
-runLinesSmoke = do
-  let input = "Hello\nWorld\n\n"
-  putStrLn "Input: \{show input}"
-  let reference = lines input
-  putStrLn "Reference: \{show reference}"
-  let (output, rest) = extract $ runLines input lines'
-  putStrLn "Output: \{show output}"
-  putStrLn "Rest: \{show rest}"
-  pure $ output == reference && null rest
-  where
-    lines' : Eff [Lines] (List String)
-    lines' = do
-      Just next <- take
-        | _ => pure []
-      map (next ::) lines'

src/SSG/Djot/Render.idr

@@ -1,57 +0,0 @@
-||| Render Djot to HTML
-module SSG.Djot.Render
-
-import SSG.HTML
-import SSG.Djot.Inline
-import SSG.Djot.Block
-
-import Data.List
-import Data.Nat
-
-||| Render a single inline element as HTML
-export
-renderInline : Inline -> Maybe (t ** Html t)
--- FIXME: escape text
-renderInline (Text text) = Just (_ ** Text text)
-renderInline SoftLineBreak = Nothing
-renderInline HardLineBreak = Just (_ ** Void "br" [])
-
-||| Render a list of inline elments to html
-export
-renderInlines : List Inline -> (types ** DList _ Html types)
-renderInlines xs = fromList . catMaybes $ map renderInline xs
-
-||| Render a single block element as HTML
-export
-renderBlock : Block t -> (t ** Html t)
-
-||| Render a list of block level elements to html
-export
-renderBlocks : {types: _} -> DList _ Block types -> (types' ** DList _ Html types')
-
-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
-
-||| Render a complete html document from a list of block level elements
-export
-renderDocument : {types : _} -> DList _ Block types -> Html "html"
-renderDocument xs =
-  Normal "html" ["lang" =$ "en"] [
-    Normal "body" [] (snd (renderBlocks xs))
-  ]

src/SSG/HTML.idr

@@ -63,8 +63,8 @@ namespace Html
     if length attributes > 0
       then
         let attrs = joinBy " " $ map toString attributes
-        in "\{indent}<\{type} \{attrs}>"
+        in "<\{type} \{attrs} />"
-      else "\{indent}<\{type}>"
+      else "<\{type} />"
   viewIndented indent_level (Normal type attributes {content_types} contents) =
     let indent = replicate (indent_level * 2) ' ' in
     -- Special handling if the tag contains exactly one `Text` element, we won't
@@ -123,10 +123,10 @@ namespace Html
   TagType' : (type : String) -> {auto prf : IsValidTag type} -> Type
   TagType' type {prf} = TagType prf
 
-  -- ||| Smart constructor for tags
+  ||| Smart constructor for tags
-  -- public export
+  public export
-  -- tag : (type : String) -> {auto prf : IsValidTag type} -> TagType prf
+  tag : (type : String) -> {auto prf : IsValidTag type} -> TagType prf
-  -- tag type {prf = (PVoid type)} = Void type
+  tag type {prf = (PVoid type)} = Void type
-  -- tag type {prf = (PRawText type)} = RawText type
+  tag type {prf = (PRawText type)} = RawText type
-  -- tag type {prf = (PEscapableRawText type)} = RawText type
+  tag type {prf = (PEscapableRawText type)} = RawText type
-  -- tag type {prf = (PNormal type)} = Normal type
+  tag type {prf = (PNormal type)} = Normal type

src/SSG/Parser/Core.idr

@@ -0,0 +1 @@
+module SSG.Parser.Core

src/SSG/Parser/Markdown.idr

@@ -0,0 +1 @@
+module SSG.Parser.Markdown

test/Main.idr

@@ -1,9 +0,0 @@
-module Main
-
-import Test.Golden.RunnerHelper
-
-main : IO ()
-main = goldenRunner
-  [ "Hedgehog Tests" `atDir` "hedgehog"
-  , "Djot -> HTML Tests" `atDir` "djotToHtml"
-  ]

test/djotToHtml/001-paragraph/Main.idr

@@ -1,18 +0,0 @@
-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

test/djotToHtml/001-paragraph/expected

@@ -1,33 +0,0 @@
-<!DOCTYPE HTML>
-<html lang=en>
-  <body>
-    <p>Hello World!</p>
-    <p>Hello Alice!</p>
-    <p>
-      A Multi-line
-      Paragraph
-    </p>
-    <p>Two line breaks</p>
-    <p>
-      A multiline paragraph
-      with some indentation
-    </p>
-    <p>
-      This is a hard
-      <br>
-      line break
-    </p>
-    <p>
-      And again
-      <br>
-      with some spaces afterwards
-    </p>
-    <p>
-      And now we
-      mix soft
-      <br>
-      and hard
-      linebreaks
-    </p>
-  </body>
-</html>

test/djotToHtml/001-paragraph/pack.toml

@@ -1,5 +0,0 @@
-[custom.all.SSG]
-type = "local"
-path = "../../.."
-ipkg = "SSG.ipkg"
-test = "test/test.ipkg"

test/djotToHtml/001-paragraph/run

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

test/djotToHtml/001-paragraph/test.dj

@@ -1,23 +0,0 @@
-Hello World!
-
-Hello Alice!
-
-A Multi-line
-Paragraph
-
-
-Two line breaks
-
-A multiline paragraph
-  with some indentation
-
-This is a hard\
-line break
-
-And again\   
-with some spaces afterwards
-
-And now we
-mix soft\ 
-and hard
-linebreaks

test/djotToHtml/001-paragraph/test.ipkg

@@ -1,9 +0,0 @@
-package a-test
-
-depends = SSG
-        , hedgehog
-        , eff
-
-main = Main
-
-executable = test

test/djotToHtml/002-headings/Main.idr

@@ -1,18 +0,0 @@
-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

test/djotToHtml/002-headings/expected

@@ -1,44 +0,0 @@
-<!DOCTYPE HTML>
-<html lang=en>
-  <body>
-    <h1>Level 1 Heading</h1>
-    <h2>Level 2 Heading</h2>
-    <h3>Level 3 Heading</h3>
-    <h4>Level 4 Heading</h4>
-    <h5>Level 5 Heading</h5>
-    <h6>Level 6 Heading</h6>
-    <p>####### Level 7 Not a heading</p>
-    <h1>
-      Multiline heading
-      with prefix
-    </h1>
-    <h1>
-      Multiline heading
-      with prefix and some extra whitespace
-    </h1>
-    <h2>
-      Level 2 multiline heading
-      with prefix
-    </h2>
-    <h1>
-      Multiline heading
-      with no prefix
-    </h1>
-    <h2>
-      Level 2 multiline heading
-      with no prefix
-    </h2>
-    <h1>
-      Unprefixed multiline heading
-      with some indentation
-    </h1>
-    <h1>
-      Heading level 1
-      # With a level 2 right after it (this line shouldn't be a heading)
-    </h1>
-    <h2>
-      Heading level 2
-      With a level 1 right after it (this line shouldn't be a heading)
-    </h2>
-  </body>
-</html>

test/djotToHtml/002-headings/pack.toml

@@ -1,5 +0,0 @@
-[custom.all.SSG]
-type = "local"
-path = "../../.."
-ipkg = "SSG.ipkg"
-test = "test/test.ipkg"

test/djotToHtml/002-headings/run

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

test/djotToHtml/002-headings/test.dj

@@ -1,38 +0,0 @@
-# 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)

test/djotToHtml/002-headings/test.ipkg

@@ -1,9 +0,0 @@
-package a-test
-
-depends = SSG
-        , hedgehog
-        , eff
-
-main = Main
-
-executable = test

test/hedgehog/001-lines/Main.idr

@@ -1,28 +0,0 @@
-module Main
-
-import SSG.Djot.Lines
-
-import Control.Eff
-import Data.String
-import Hedgehog
-
-lines' : Eff [Lines] (List String)
-lines' = do
-  Just next <- take
-    | _ => pure []
-  map (next ::) lines'
-
-propLinesEquiv : Property
-propLinesEquiv = property $ do
-  str <- forAll $ string (linear 0 256) ascii
-  let std_lines = lines str
-  let (our_lines, rest) = extract $ runLines str lines'
-  our_lines === std_lines
-
-main : IO ()
-main = test $
-  [ MkGroup
-      "Lines effect"
-      [ ("Lines effect equivalent to lines", propLinesEquiv)
-      ]
-  ]

test/hedgehog/001-lines/expected

@@ -1,3 +0,0 @@
-━━━ Lines effect ━━━
-  ✓ Lines effect equivalent to lines passed 1000 tests.
-  ✓ 1 succeeded.

test/hedgehog/001-lines/pack.toml

@@ -1,5 +0,0 @@
-[custom.all.SSG]
-type = "local"
-path = "../../.."
-ipkg = "SSG.ipkg"
-test = "test/test.ipkg"

test/hedgehog/001-lines/run

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

test/hedgehog/001-lines/test.ipkg

@@ -1,9 +0,0 @@
-package a-test
-
-depends = SSG
-        , hedgehog
-        , eff
-
-main = Main
-
-executable = test

test/src/Main.idr

@@ -0,0 +1,4 @@
+module Main
+
+main : IO ()
+main = putStrLn "Test successful!"

test/test.ipkg

@@ -14,7 +14,6 @@ authors = "Nathan McCarty"
 
 -- packages to add to search path
 depends = SSG
-        , golden-runner-helper
 
 -- modules to install
 -- modules =
@@ -25,7 +24,7 @@ main = Main
 -- name of executable
 executable = "SSG-test"
 -- opts =
--- sourcedir = "."
+sourcedir = "src"
 -- builddir =
 -- outputdir =
 

todo.org

@@ -2,67 +2,5 @@
 ** TODO Special handling for =pre= in =view=
 ** TODO Smart spec compliance for =attribute=
 Probably want to refine the attribute and value strings, and be smarter about how we choose to quote the value string.
-** TODO Don't generate any further indent once we are already inside a =p=
-** TODO Text escaping function
 ** NO Move =Raw= out of =Tag=
 Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make sense
-* Parser Core
-** TODO Refine =location= in =ParserLocation=
-** TODO Error messages
-** TODO Combinators for predictive parsing
-* Djot [4/40]
-:PROPERTIES:
-:COOKIE_DATA: recursive
-:END:
-** Parsing [4/34]
-*** Block Level
-**** TODO Block Quote
-**** TODO List Item
-**** TODO List
-**** TODO Code Block
-**** TODO Thematic Break
-**** TODO Raw Block
-**** TODO Div
-**** TODO Pipe Table
-**** TODO Reference Link Definition
-**** TODO Footnote
-**** TODO Block Attributes
-**** TODO Heading Links
-**** DONE Paragraph
-**** DONE Heading
-*** Inline
-**** TODO Escaped Text
-**** TODO Link
-**** TODO Image
-**** TODO Autolink
-**** TODO Verbatim
-**** TODO Emphasis/Strong
-**** TODO Highlighted
-**** TODO Super/subscript
-**** TODO Insert/delete
-**** TODO Smart Punctuation
-**** TODO Math
-**** TODO Footnote Reference
-**** TODO Comment
-**** TODO Symbols
-**** TODO Raw Inline
-**** TODO Inline Attributes
-**** DONE Ordinary Text
-**** DONE Linebreak
-*** 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