From 69f198dbd39824a113182a08f3fb2318eb046c3e Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 20 Feb 2025 22:20:30 -0500 Subject: [PATCH] [new] Support literate Djot files Djot is a markup format that is derived from CommonMark, it's code block syntax is identical to CommonMark's, so we can support it as a CommonMark style literate formate by just adding the file extension. --- CHANGELOG_NEXT.md | 3 +++ CONTRIBUTORS | 1 + docs/source/reference/literate.rst | 2 +- src/Parser/Unlit.idr | 2 +- tests/idris2/literate/literate020/IEdit.dj | 29 ++++++++++++++++++++++ tests/idris2/literate/literate020/expected | 4 +++ tests/idris2/literate/literate020/input | 2 ++ tests/idris2/literate/literate020/run | 3 +++ 8 files changed, 44 insertions(+), 2 deletions(-) create mode 100644 tests/idris2/literate/literate020/IEdit.dj create mode 100644 tests/idris2/literate/literate020/expected create mode 100644 tests/idris2/literate/literate020/input create mode 100755 tests/idris2/literate/literate020/run diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 0e22fb81ba..8b835501e4 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -122,6 +122,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO with `_builtin.` (eg `_builtin.CONS`). This allows the identity optimisation to optimise conversions between list-shaped things. +* [Djot](https://djot.net/) files can now be compiled as CommonMark style + Literate Idris files. + ### Backend changes #### RefC Backend diff --git a/CONTRIBUTORS b/CONTRIBUTORS index e5e12b037a..b5b5e4bed9 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -56,6 +56,7 @@ Michael Morgan Milan Kral Molly Miller Mounir Boudia +Nathan McCarty Nick Drozd Nicolas Biri Niklas Larsson diff --git a/docs/source/reference/literate.rst b/docs/source/reference/literate.rst index 92cdccd30a..8d57b9c63e 100644 --- a/docs/source/reference/literate.rst +++ b/docs/source/reference/literate.rst @@ -86,7 +86,7 @@ Each of the following markup is recognised regardless of case: CommonMark ********** -We treat files with an extension of ``.md`` and ``.markdown`` as CommonMark style literate files. +We treat Markdown files with an extension of ``.md`` or ``.markdown`` and Djot files with an extension of ``.dj`` as CommonMark style literate files. + CommonMark source blocks for idris sans options are recognised as visible code blocks:: diff --git a/src/Parser/Unlit.idr b/src/Parser/Unlit.idr index 0581e620bd..2d3ec81f69 100644 --- a/src/Parser/Unlit.idr +++ b/src/Parser/Unlit.idr @@ -33,7 +33,7 @@ styleCMark : LiterateStyle styleCMark = MkLitStyle [("```idris", "```"), ("~~~idris", "~~~"), ("")] Nil - [".md", ".markdown"] + [".md", ".markdown", ".dj"] export styleTeX : LiterateStyle diff --git a/tests/idris2/literate/literate020/IEdit.dj b/tests/idris2/literate/literate020/IEdit.dj new file mode 100644 index 0000000000..ccbc3adad8 --- /dev/null +++ b/tests/idris2/literate/literate020/IEdit.dj @@ -0,0 +1,29 @@ +```idris +data Vect : Nat -> Type -> Type where + Nil : Vect Z a + (::) : a -> Vect k a -> Vect (S k) a +``` + + + +```idris +dupAll : Vect n a -> Vect n (a, a) +dupAll xs = zipHere xs xs + where + zipHere : forall n . Vect n a -> Vect n b -> Vect n (a, b) +``` + + + + + +```idris +showFooBar : Foobar -> String +showFooBar MkFoo = "MkFoo" +``` diff --git a/tests/idris2/literate/literate020/expected b/tests/idris2/literate/literate020/expected new file mode 100644 index 0000000000..09bb907f15 --- /dev/null +++ b/tests/idris2/literate/literate020/expected @@ -0,0 +1,4 @@ +1/1: Building IEdit (IEdit.dj) +Main> zipHere [] [] = [] + zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys +Main> Bye for now! diff --git a/tests/idris2/literate/literate020/input b/tests/idris2/literate/literate020/input new file mode 100644 index 0000000000..fa4e351191 --- /dev/null +++ b/tests/idris2/literate/literate020/input @@ -0,0 +1,2 @@ +:gd 15 zipHere +:q diff --git a/tests/idris2/literate/literate020/run b/tests/idris2/literate/literate020/run new file mode 100755 index 0000000000..f9b9e6f9a8 --- /dev/null +++ b/tests/idris2/literate/literate020/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +idris2 IEdit.dj < input