diff --git a/blog b/blog index 5051bef..6784af9 100755 --- a/blog +++ b/blog @@ -284,21 +284,6 @@ multi MAIN( $db.write: $db-dir; } -#| Update the posted-at time on a post to the current time -multi MAIN( - "post", - "now", - #| The id of the post to update the posted-at time - Int $id, - #| The path of the database directory - IO::Path(Str) :$db-dir = $default-db-dir, -){ - my $db = read-db $db-dir; - my $post = $db.posts{$id.Int}; - $post.posted-at = DateTime.now; - $db.write: $db-dir; -} - #| Create a new series multi MAIN( "series", diff --git a/lib/DB/Post.rakumod b/lib/DB/Post.rakumod index d231956..c1e98c7 100644 --- a/lib/DB/Post.rakumod +++ b/lib/DB/Post.rakumod @@ -16,7 +16,6 @@ IO::Path:D $.source #| The time to display for the creation of the post has DateTime:D $.posted-at - is rw is required is json( :to-json(*.Str), diff --git a/lib/Render/Head.rakumod b/lib/Render/Head.rakumod index 22fa4ee..c93c3ff 100644 --- a/lib/Render/Head.rakumod +++ b/lib/Render/Head.rakumod @@ -47,6 +47,7 @@ sub site-header(BlogMeta:D $meta) is export { sub header-link($name, $path, $icon) { a :href("$path"), [ icon $icon; + ' '; span $name; ] } diff --git a/lib/Render/Util.rakumod b/lib/Render/Util.rakumod index 475a79a..79ece58 100644 --- a/lib/Render/Util.rakumod +++ b/lib/Render/Util.rakumod @@ -10,9 +10,7 @@ sub show-html($html) is export { # Work around HTML::Functional automatically putting newlines between tags $out ~~ s:g/'' \v+ ''/<\/i>/; $out ~~ s:g/\v+ ''/<\/a>/; - $out ~~ s:g/\s+ ',' \s+ '' \s* '
  '/
<\/i>Unit Test<\/span>
/;
+   $out ~~ s:g/',' \v+ ' [!NOTE]
 > As this is a literate Idris document, and we haven't defined our `printf`
@@ -34,202 +32,14 @@ equivalent:
 
 ```idris
 failing
-  printf "%s %d %2d" "hello" 1 2
+  example_usage : String
+  example_usage = printf "%s %d %02d" "hello" 1 2
 ```
 
-Idris lacks a dedicated facility for variadics, but we can call functions in
-type signatures, Idris allows us to manipulate types as first class values, and
-we can use the runtime values of previous arguments to the function we are
-defining as arguments to our type-level function.
 
-To get our variadic `printf` function, we can parse our format string into a
-data structure, then pass that data structure into a type-level function that
-calculates the rest of the type signature of our `printf` function based on its
-contents.
 
 ## Parsing a Format String
 
-First, we need a data structure to describe our format string. We define the
-`Format` data type, with constructors for each of the format specifiers we will
-be supporting, as well as a constructor to hold literal components.
-
-```idris
-data Format : Type where
-  ||| A slot that should be filled in with a number
-  Number : (next : Format) -> Format
-  ||| A slot that should be filled  in with a number, padded to a certian number
-  ||| of digits
-  PaddedNumber : (digits : Nat) -> (next : Format) -> Format
-  ||| A slot that should be filled in with a string
-  Str : (next : Format) -> Format
-  ||| A literal component of the format string that should not be interpolated
-  Literal : (literal : String) -> (next : Format) -> Format
-  ||| The end of the format string
-  End : Format
-```
-
-We'll need to be able to parse numbers for our `PaddedNumber` constructor, so
-we'll write a little helper function to handle that component of the parsing.
-Simply keep pulling off characters, converting them to integers by shifting
-their ordinal values.
-
-> [!WARNING]
-> On Idris 2's chez scheme backend, these are unicode ordinals, where the digit
-> characters are in numerical order, but the values are backend dependent and
-> this code is not guaranteed to work properly on other backends.
-
-```idris
-parseNumber : (xs : List Char) -> (acc : Nat) -> (Nat, List Char)
-parseNumber [] acc = (acc, [])
-parseNumber (x :: xs) acc = 
-  if isDigit x
-    then let value = cast $ (ord x) - (ord '0')
-    in parseNumber xs (acc * 10 + value)
-    else (acc, x :: xs)
-```
-
-We'll also want another one to scoop up a literal into a `List Char`, continuing
-until we hit the end of the string or the next `%`. This is optional, we could
-have each literal consist of an individual char, but we will go ahead and group
-them together.
-
-```idris
-parseLiteral : (xs : List Char) -> (List Char, List Char)
-parseLiteral [] = ([], [])
-parseLiteral ('%' :: xs) = ([], '%' :: xs)
-parseLiteral (x :: xs) = 
-  let (literal, rest) = parseLiteral xs
-  in (x :: literal, rest)
-```
-
-Parse our format string into our `Format` data structure. The specifics of the
-parsing here aren't really material to the main point of this article, but we
-use a basic pattern matching approach, calling into our helper functions as
-appropriate. 
-
-```idris
-parseFormat : (xs : List Char) -> Maybe Format
-parseFormat [] = Just End
--- A `%` has to come before a specifier
-parseFormat ('%' :: []) = Nothing
-parseFormat ('%' :: (x :: xs)) = 
-  if isDigit x
-    -- Invoke parseNumber to get our padding specifier
-    then let (digits, rest) = parseNumber (x :: xs) 0
-    in case rest of
-      -- A padding specifier has to come before something
-      [] => Nothing
-      ('d' :: ys) => do
-        rest <- parseFormat ys
-        Just $ PaddedNumber digits rest
-      -- A padding specifier is only valid before a number specifier
-      (y :: ys) => Nothing
-    -- Parse as an unpadded specifier
-    else case x of
-      'd' => do
-        rest <- parseFormat xs
-        Just $ Number rest
-      's' => do
-        rest <- parseFormat xs
-        Just $ Str rest
-      -- Any other character here is an invalid specifier
-      _ => Nothing
-parseFormat (x :: xs) = 
-  let (literal, rest) = parseLiteral (x :: xs)
-  in do
-    rest <- parseFormat rest
-    Just $ Literal (pack literal) rest
-```
-
 ## Calculating a Type From a Format String
 
-```idris 
-PrintfType' : Format -> Type
-PrintfType' (Number next) =
-  (num : Nat) -> PrintfType' next
-PrintfType' (PaddedNumber digits next) =
-  (num : Nat) -> PrintfType' next
-PrintfType' (Str next) = 
-  (str : String) -> PrintfType' next
-PrintfType' (Literal literal next) = 
-  PrintfType' next
-PrintfType' End = String
-
-PrintfType : Maybe Format -> Type
-PrintfType Nothing = Void -> String
-PrintfType (Just x) = PrintfType' x
-```
-
 ## printf
-
-### With the Format Structure
-
-```idris hide
-left_pad : (len : Nat) -> (pad : Char) -> (str : String) -> String
-left_pad len pad str = 
-  let cs = unpack str
-  in if length cs < len
-    then pack $ replicate (len `minus` length cs) pad ++ cs
-    else str
-```
-
-```idris
-printfFmt : (fmt : Maybe Format) -> (acc : String) -> PrintfType fmt
-printfFmt Nothing acc = 
-  \void => absurd void
-printfFmt (Just x) acc = printfFmt' x acc
-  where 
-    printfFmt' : (fmt : Format) -> (acc : String) -> PrintfType' fmt
-    printfFmt' (Number next) acc = 
-      \i => printfFmt' next (acc ++ show i)
-    printfFmt' (PaddedNumber digits next) acc = 
-      \i => printfFmt' next (acc ++ left_pad digits '0' (show i))
-    printfFmt' (Str next) acc =
-      \str => printfFmt' next (acc ++ str)
-    printfFmt' (Literal literal next) acc = 
-      printfFmt' next (acc ++ literal)
-    printfFmt' End acc = acc
-```
-
-### With a Format String
-
-```idris
-printf : (fmt : String) -> PrintfType (parseFormat (unpack fmt))
-printf fmt = printfFmt _ ""
-```
-
-We can call `printf` as expected, with the number of and types of the arguments
-being determined by the provided format string:
-
-```idris hide
--- @@test printf hello world
-helloWorld : IO Bool
-helloWorld = do
-  pure $
-```
-
-```idris
-  printf "%s %s%s %3d %d" "Hello" "world" "!" 1 23 == "Hello world! 001 23"
-```
-
-It will even fail to compile if you attempt to provide arguments to an invalid
-format string, which we can demonstrate by trying to apply a padding modifier to
-a string specifier:
-
-> [!NOTE]
-> `failing` blocks have an additional feature, they will trigger a compiler
-> error if their contents _do_ compile successfully.
-
-```idris
-failing
-  printf "Hello %s %3s" "world" "!"
-```
-
-## Working With Run-Time Format Strings
-
-## Conclusions
-
-### Why this API isn't really a great idea
-
- 
-
diff --git a/projects/Markdown/About.md b/projects/Markdown/About.md
index 1b76ca4..0ac75d5 100644
--- a/projects/Markdown/About.md
+++ b/projects/Markdown/About.md
@@ -55,16 +55,6 @@ I've written a few libraries and utilities for Idris 2 already:
   provides comment-based unit testing capability. Currently written in Raku, I
   hope to eventually rewrite this in idris.
 
-### Raku
-
-- [blog](https://git.stranger.systems/thatonelutenist/website)
-
-  The static site generator powering this blog. This is a horribly cursed tangle
-  of ill-thought-through raku code that is not meant to be reused. Feel free to
-  take a look and maybe take inspiration from it, or at the very least feel
-  better about your own just-get-it-done code, but don't let me catch you
-  forking it.
-
 ### Books
 
 - [Idris by Highly Contrived Example](https://static.stranger.systems/idris-by-contrived-example/)
diff --git a/resources/admonitions.css b/resources/admonitions.css
index 0c57da9..801cf4d 100644
--- a/resources/admonitions.css
+++ b/resources/admonitions.css
@@ -12,7 +12,7 @@
     color: var(--fg-1);
     padding: 0.5rem;
     border-radius: 1rem;
-    border: solid 0.35rem;
+    border: solid 0.5rem;
     margin-top: var(--box-margin-vert);
     margin-bottom: var(--box-margin-vert);
 }
@@ -29,6 +29,8 @@
 .warning .title p,
 .caution .title p {
     font-size: 0;
+    display: inline-block;
+    position: relative;
 }
 .note .title p::before,
 .tip .title p::before,
@@ -36,7 +38,8 @@
 .warning .title p::before,
 .caution .title p::before {
     font-family: 'boxicons' !important;
-    font-size: 4rem;
+    font-size: 3rem;
+    display: inline-block;
 }
 
 /* Notes */
@@ -65,17 +68,17 @@
 }
 /* Warnings */
 .warning {
-    border-color: var(--yellow);
+    border-color: var(--orange);
 }
 .warning .title p::before {
-    content: "\eac5";
-    color: var(--yellow);
+    content: "\e9a3";
+    color: var(--orange);
 }
 /* Cautions */
 .caution {
     border-color: var(--red);
 }
 .caution .title p::before {
-    content: "\eac6";
+    content: "\ee87";
     color: var(--red);
 }
diff --git a/resources/code.css b/resources/code.css
index a3e1758..18edce7 100644
--- a/resources/code.css
+++ b/resources/code.css
@@ -6,7 +6,6 @@ code {
 /* Styling for inline code blocks */
 :not(pre) > code {
     padding: 0 0.25rem;
-    border-radius: 0.25rem;
 }
 
 /* Styling for fenced code blocks */
@@ -19,30 +18,4 @@ pre > code {
 }
 pre {
     width: 90%;
-    box-sizing: border-box;
-}
-
-/* Styling for unit tests */
-.unit-test {
-    width: 90%;
-    display: flex;
-    flex-direction: column;
-    align-items: center;
-    padding: 1rem;
-    border-radius: 0.55rem / 0.5rem;
-    box-sizing: border-box;
-}
-.unit-test > span {
-    display: flex;
-    flex-direction: row;
-    align-items: center;
-    padding: 0.5rem;
-    border-radius: 0.55rem / 0.5rem;
-}
-.unit-test > pre {
-    width: auto;
-}
-.unit-test i {
-    font-size: 1.5rem;
-    margin-right: 0.5rem;
 }
diff --git a/resources/colors.css b/resources/colors.css
index 5c9ec9c..42db252 100644
--- a/resources/colors.css
+++ b/resources/colors.css
@@ -78,16 +78,6 @@ a:visited {
 blockquote {
   background-color: var(--bg-1);
 }
-.unit-test {
-  background-color: var(--bg-1);
-}
-.unit-test > span {
-  background-color: var(--bg-2);
-  color: var(--fg-1);
-}
-.unit-test i {
-  color: var(--green);
-}
 
 /* Colorization for idris code blocks */
 code {