From 2ce4579e08a16ea2ff9b8780ef24ebdb0b05b9b4 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 05:13:19 -0500 Subject: [PATCH] Basic Html Rendering --- SSG.ipkg | 2 ++ bin/Djot.ipkg | 47 +++++++++++++++++++++++++++ bin/src/Djot.idr | 21 +++++++++++++ pack.toml | 5 +++ src/SSG/Djot.idr | 13 ++++++++ src/SSG/Djot/Block.idr | 2 ++ src/SSG/Djot/Inline.idr | 12 +++---- src/SSG/Djot/Render.idr | 70 +++++++++++++++++++++++++++++++++++++++++ todo.org | 4 +-- 9 files changed, 168 insertions(+), 8 deletions(-) create mode 100644 bin/Djot.ipkg create mode 100644 bin/src/Djot.idr create mode 100644 src/SSG/Djot/Render.idr diff --git a/SSG.ipkg b/SSG.ipkg index adfdb9e..1df6058 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -14,6 +14,7 @@ authors = "Nathan McCarty" -- packages to add to search path depends = structures + , tailrec , eff , refined , elab-util @@ -25,6 +26,7 @@ modules = SSG.Parser.Core , SSG.Djot.Common , SSG.Djot.Inline , SSG.Djot.Block + , SSG.Djot.Render , SSG.HTML , SSG.HTML.ElementTypes diff --git a/bin/Djot.ipkg b/bin/Djot.ipkg new file mode 100644 index 0000000..bc3a2dc --- /dev/null +++ b/bin/Djot.ipkg @@ -0,0 +1,47 @@ +package Djot +version = 0.1.0 +authors = "Nathan McCarty" +-- maintainers = +-- license = +-- brief = +-- readme = +-- homepage = +-- sourceloc = +-- bugtracker = + +-- the Idris2 version required (e.g. langversion >= 0.5.1) +-- langversion + +-- packages to add to search path +depends = SSG + +-- modules to install +-- modules = + +-- main file (i.e. file to load at REPL) +main = Djot + +-- name of executable +executable = "djot" +-- opts = +sourcedir = "src" +-- builddir = +-- outputdir = + +-- script to run before building +-- prebuild = + +-- script to run after building +-- postbuild = + +-- script to run after building, before installing +-- preinstall = + +-- script to run after installing +-- postinstall = + +-- script to run before cleaning +-- preclean = + +-- script to run after cleaning +-- postclean = diff --git a/bin/src/Djot.idr b/bin/src/Djot.idr new file mode 100644 index 0000000..3bdfc57 --- /dev/null +++ b/bin/src/Djot.idr @@ -0,0 +1,21 @@ +module Djot + +import System +import System.File + +import SSG.Djot +import SSG.HTML + +main : IO () +main = do + args <- getArgs + case args of + [_, file] => do + Right contents <- readFile file + | Left err => printLn err + let parsed = djot contents + printLn parsed + putStr . render $ renderHtml parsed + _ => do + putStrLn "?" + exitFailure diff --git a/pack.toml b/pack.toml index eed6e77..303ca46 100644 --- a/pack.toml +++ b/pack.toml @@ -4,6 +4,11 @@ path = "." ipkg = "SSG.ipkg" test = "test/test.ipkg" +[custom.all.Djot] +type = "local" +path = "bin" +ipkg = "Djot.ipkg" + [custom.all.SSG-test] type = "local" path = "test" diff --git a/src/SSG/Djot.idr b/src/SSG/Djot.idr index 274ed75..84636b1 100644 --- a/src/SSG/Djot.idr +++ b/src/SSG/Djot.idr @@ -1,4 +1,17 @@ module SSG.Djot +import SSG.Parser.Util + +import Control.Eff + import public SSG.Djot.Inline as SSG.Djot import public SSG.Djot.Block as SSG.Djot +import public SSG.Djot.Render as SSG.Djot + +export +||| Parse a djot document +djot : String -> List Block +djot str = + case runPS blocks str of + Left _ => [] + Right x => x diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr index f3f8522..14cdbed 100644 --- a/src/SSG/Djot/Block.idr +++ b/src/SSG/Djot/Block.idr @@ -97,6 +97,7 @@ heading = do -- Overall Block Parser -- -------------------------- +export block : PS Block block = do -- eat up any blank lines @@ -106,6 +107,7 @@ block = do , paragraph ] +export blocks : PS (List Block) blocks = many block diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr index 7573062..eed029d 100644 --- a/src/SSG/Djot/Inline.idr +++ b/src/SSG/Djot/Inline.idr @@ -22,7 +22,7 @@ data Inline : Type where HardLineBreak : Inline SoftLineBreak : Inline NonBreakingSpace : Inline - Text : (c : Char) -> Inline + Text : (c : String) -> Inline %runElab derive "Inline" [Show, Eq] @@ -69,13 +69,13 @@ softLineBreak = do escapedText : PS Inline escapedText = do c <- escapedChar - pure $ Text c + pure $ Text (singleton c) -- Any non-line-ending character can be part of regular text text : PS Inline text = do c <- nonTerminal - pure $ Text c + pure $ Text (singleton c) --------------------------- -- Overall Inline Parser -- @@ -113,7 +113,7 @@ inlineFromString : String -> List (Inline) inlineFromString str with (asList str) inlineFromString "" | [] = [] inlineFromString (strCons c str) | (c :: x) = - Text c :: inlineFromString str | x + Text (singleton c) :: inlineFromString str | x export inlineFromString' : String -> List1 (Inline) @@ -130,13 +130,13 @@ inlineFromString' str = inlineTextSmoke : IO Bool inlineTextSmoke = let input = "Hello World!" in - golden input (map Text . unpack $ input) (map forget inline) + golden input (map (Text . singleton) . unpack $ input) (map forget inline) -- @@test Escaped Text inlineEscapedSmoke : IO Bool inlineEscapedSmoke = let input = "Hello\\n\\*World" - ref = inlineFromString "Hello" ++ [Text '\n', Text '*'] ++ inlineFromString "World" + ref = inlineFromString "Hello" ++ [Text "\n", Text "*"] ++ inlineFromString "World" in golden input ref (map forget inline) -- @@test Hard Line Break diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr new file mode 100644 index 0000000..7bc1b06 --- /dev/null +++ b/src/SSG/Djot/Render.idr @@ -0,0 +1,70 @@ +module SSG.Djot.Render + +import SSG.HTML + +import SSG.Djot.Inline +import SSG.Djot.Block + +import Data.String +import Data.List1 + +import Structures.Dependent.DList + +export +renderInline : Inline -> (type : String ** Html type) +renderInline HardLineBreak = + (_ ** Void "br" []) +renderInline SoftLineBreak = + (_ ** Text "\n") +renderInline NonBreakingSpace = + (_ ** Text " ") +renderInline (Text c) = + (_ ** Text c) + +-- BUG: Coverage checker bug here? +partial +combineTexts : (types : List String ** DList _ Html types) + -> (types' : List String ** DList _ Html types') +combineTexts (_ ** []) = (_ ** []) +combineTexts xs@(_ ** (elem :: [])) = xs +combineTexts (_ ** Text content :: (Text str :: rest)) = + combineTexts (_ ** Text (content ++ str) :: rest) +combineTexts (_ ** Text content :: (next :: rest)) = + let (_ ** rest) = combineTexts (_ ** (next :: rest)) + in (_ ** Text content :: rest) +combineTexts (_ ** (x :: (next :: rest))) = + let (_ ** rest) = combineTexts (_ ** (next :: rest)) + in (_ ** x :: rest) + +export +renderInlines : List Inline -> (types : List String ** DList _ Html types) +renderInlines xs = assert_total $ + combineTexts . fromList . map renderInline $ xs + +headingLevel : HeaderLevel -> (h : String ** IsNormal h) +headingLevel H1 = ("h1" ** IsH1) +headingLevel H2 = ("h2" ** IsH2) +headingLevel H3 = ("h3" ** IsH3) +headingLevel H4 = ("h4" ** IsH4) +headingLevel H5 = ("h5" ** IsH5) +headingLevel H6 = ("h6" ** IsH6) + +export +renderBlock : Block -> (type : String ** Html type) +renderBlock (Paragraph contents) = + let (_ ** xs) = renderInlines $ forget contents + in (_ ** Normal "p" [] xs) +renderBlock (Heading level contents) = + let (_ ** xs) = renderInlines $ forget contents + (level ** _ ) = headingLevel level + in (_ ** Normal level [] xs) + +export +renderBlocks : List Block -> (types : List String ** DList _ Html types) +renderBlocks xs = fromList $ map renderBlock xs + +export +renderHtml : List Block -> Html "html" +renderHtml xs = + let (_ ** xs) = renderBlocks xs + in Normal "html" ["lang" =$ "en"] xs diff --git a/todo.org b/todo.org index aad08f1..bb2b3c9 100644 --- a/todo.org +++ b/todo.org @@ -8,7 +8,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 [4/42] +* Djot [5/42] :PROPERTIES: :COOKIE_DATA: recursive :END: @@ -50,7 +50,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Footnote **** TODO Block attributes **** TODO Links to headings -** TODO Rendering +** DONE Rendering ** TODO Predictive parsing ** TODO Support all types of whitespace *** TODO Escaping