From 79c74426c1c3f424fa296cc2c4c36ba3159c38c3 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 21 Feb 2025 03:56:30 -0500
Subject: [PATCH] Basic Heading Parsing

---
 src/SSG/Djot.idr | 71 +++++++++++++++++++++++++++++++++++++++++++++++-
 todo.org         |  7 ++---
 2 files changed, 73 insertions(+), 5 deletions(-)

diff --git a/src/SSG/Djot.idr b/src/SSG/Djot.idr
index 131e2bf..41924ca 100644
--- a/src/SSG/Djot.idr
+++ b/src/SSG/Djot.idr
@@ -29,9 +29,45 @@ data Inline : Type where
 
 %runElab derive "Inline" [Show, Eq]
 
+public export
+data HeaderLevel : Type where
+  H1 : HeaderLevel
+  H2 : HeaderLevel
+  H3 : HeaderLevel
+  H4 : HeaderLevel
+  H5 : HeaderLevel
+  H6 : HeaderLevel
+
+%runElab derive "HeaderLevel" [Eq]
+
+export
+Show HeaderLevel where
+  show H1 = "1"
+  show H2 = "2"
+  show H3 = "3"
+  show H4 = "4"
+  show H5 = "5"
+  show H6 = "6"
+
+namespace HeaderLevel
+  public export
+  integerToHeader : Integer -> Maybe HeaderLevel
+  integerToHeader 1 = Just H1
+  integerToHeader 2 = Just H2
+  integerToHeader 3 = Just H3
+  integerToHeader 4 = Just H4
+  integerToHeader 5 = Just H5
+  integerToHeader 6 = Just H6
+  integerToHeader i = Nothing
+
+  export
+  fromInteger : (x : Integer) -> {auto prf : IsJust (integerToHeader x)} -> HeaderLevel
+  fromInteger x = fromJust $ integerToHeader x
+
 public export
 data Block : Type where
   Paragraph : (contents : List1 Inline) -> Block
+  Heading : (level : HeaderLevel) -> (contents : List1 Inline) -> Block
 
 %runElab derive "Block" [Show, Eq]
 
@@ -228,6 +264,20 @@ paragraph = do
   blankLineOrEnd
   pure $ Paragraph inlines
 
+-------------
+-- Heading --
+-------------
+
+heading : PS Block
+heading = do
+  levelMarker <- atLeastOne "Expected Header Marker" $ thisString "#"
+  ws <- atLeastOne "Expected Whitespace after header marker" $ space
+  case integerToHeader (natToInteger $ length levelMarker) of
+    Nothing => throw "Invalid header length: \{show $ length levelMarker}"
+    Just level => do
+      inlines <- inline
+      pure $ Heading level inlines
+
 --------------------------
 -- Overall Block Parser --
 --------------------------
@@ -237,7 +287,8 @@ block = do
   -- eat up any blank lines
   _ <- many blankLine
   oneOfE "" [
-    paragraph
+    heading
+  , paragraph
   ]
 
 blocks : PS (List Block)
@@ -336,3 +387,21 @@ blockTwoParagraphSmoke =
       , Paragraph (inlineFromString' "Hello Again")
       ]
   in golden input ref blocks
+
+-- @@test Level 1 heading
+blockLevelOneHeadingSmoke : IO Bool
+blockLevelOneHeadingSmoke =
+  let input = "# Level 1"
+      ref = [
+        Heading 1 (inlineFromString' "Level 1")
+      ]
+  in golden input ref blocks
+
+-- @@test Level 2 heading
+blockLevelTwoHeadingSmoke : IO Bool
+blockLevelTwoHeadingSmoke =
+  let input = "## Level 2"
+      ref = [
+        Heading 2 (inlineFromString' "Level 2")
+      ]
+  in golden input ref blocks
diff --git a/todo.org b/todo.org
index 2d3b362..aad08f1 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 [3/42]
+* Djot [4/42]
 :PROPERTIES:
 :COOKIE_DATA: recursive
 :END:
@@ -32,11 +32,11 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se
 **** TODO Raw inline
 **** TODO Span
 **** TODO Inline attributes
-*** Block Syntax [1/16]
+*** Block Syntax [2/16]
 **** DONE Paragraph
 **** Heading
 ***** TODO Multiline without leading count
-***** TODO Basic
+***** DONE Basic
 **** TODO Block quote
 **** TODO List item
 **** TODO List
@@ -51,7 +51,6 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se
 **** TODO Block attributes
 **** TODO Links to headings
 ** TODO Rendering
-** Bugs [0/0]
 ** TODO Predictive parsing
 ** TODO Support all types of whitespace
 *** TODO Escaping