[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

@@ -122,6 +122,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
   with `_builtin.<TAG>` (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

CONTRIBUTORS

@@ -56,6 +56,7 @@ Michael Morgan
 Milan Kral
 Molly Miller
 Mounir Boudia
+Nathan McCarty
 Nick Drozd
 Nicolas Biri
 Niklas Larsson

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::
 

src/Parser/Unlit.idr

@@ -33,7 +33,7 @@ styleCMark : LiterateStyle
 styleCMark = MkLitStyle
               [("```idris", "```"), ("~~~idris", "~~~"), ("<!-- idris", "-->")]
               Nil
-              [".md", ".markdown"]
+              [".md", ".markdown", ".dj"]
 
 export
 styleTeX : LiterateStyle

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
+%name Vect xs, ys, zs
+-->
+
+```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
+
+data Foobar = MkFoo
+
+-->
+
+
+```idris
+showFooBar : Foobar -> String
+showFooBar MkFoo = "MkFoo"
+```

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!

tests/idris2/literate/literate020/input

@@ -0,0 +1,2 @@
+:gd 15 zipHere
+:q

tests/idris2/literate/literate020/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 IEdit.dj < input