[ literate ] Add support for typst files

CHANGELOG_NEXT.md

@@ -91,6 +91,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * `MakeFuture` primitive is removed.
 
+* Typst files can be compiled as Literate Idris
+
 ### Backend changes
 
 #### RefC Backend

docs/source/reference/literate.rst

@@ -21,14 +21,15 @@ Lexing is simple and greedy in that when consuming anything that is a code block
 This means that use of verbatim modes in a literate file will also be treated as active code.
 
 In future we should add support for literate ``LaTeX`` files, and potentially other common document formats.
-But more importantly, a more intelligent processing of literate documents using a pandoc like library in Idris such as: `Edda <https://github.com/jfdm/edda>` would also be welcome.
+But more importantly, a more intelligent processing of literate documents using a pandoc like library in Idris such as:
+`Edda <https://github.com/jfdm/edda>`_ would also be welcome.
 
 Bird Style Literate Files
 =========================
 
 We treat files with an extension of ``.lidr`` as bird style literate files.
 
-Bird notation is a classic literate mode found in Haskell, (and Orwell) in which visible code lines begin with ``>`` and hidden lines with ``<``.
+Bird notation is a classic literate mode found in Haskell (and Orwell), in which visible code lines begin with ``>`` and hidden lines with ``<``.
 Other lines are treated as documentation.
 
 
@@ -97,12 +98,34 @@ We treat files with an extension of ``.md`` and ``.markdown`` as CommonMark styl
     data Nat = Z | S Nat
     ~~~
 
-+ Comment blocks of the form ``<!-- idris\n ... \n -->`` are treated as invisible code blocks::
++ Comment blocks of the form ``<!-- idris\n ... \n-->`` are treated as invisible code blocks::
 
     <!-- idris
     data Nat = Z | S Nat
     -->
 
++ Syntax of beginnings and endings of visible and invisible code blocks must not have preceding white spaces::
+
+    Some text
+
+    ```idris
+    -- treated as visible code
+    ```
+
+    <!-- idris
+    -- treated as invisible code
+    -->
+
+    - Some list element
+
+      ```idris
+      -- code here will be ignored by the compiler
+      ```
+
+      <!-- idris
+      -- this code also will be ignored
+      -->
+
 + Code lines are not supported.
 
 + Specifications can be given using CommonMark's pre-formatted blocks (indented by four spaces) or unlabelled code blocks.::
@@ -156,3 +179,44 @@ With one such example using ``fancyverbatim`` and ``comment`` packages as::
     \usepackage{comment}
 
     \excludecomment{hidden}
+
+Typst
+*****
+
+We treat files with an extension of ``.typ`` as `Typst <https://github.com/typst/typst>`_ style literate files.
+
++ Code blocks with the Idris language set are recognised as visible code blocks::
+
+    ```idris
+    data Nat = Z | S Nat
+    ```
+
++ Comment blocks of the form ``/* idris\n ... \n*/`` are treated as invisible code blocks::
+
+    /* idris
+    data Nat = Z | S Nat
+    */
+
++ Syntax of beginnings and endings of visible and invisible code blocks must not have preceding white spaces::
+
+    Some text
+    ```idris
+    -- treated as visible code
+    ```
+    /* idris
+    -- treated as invisible code
+    */
+
+    - Some list element
+      ```idris
+      -- code here will be ignored by the compiler
+      ```
+      /* idris
+      -- this code also will be ignored
+      */
+
++ Code lines using ``#raw`` function are not supported.
+
++ Specifications can be given using ``#raw`` function with the language and block being set, e.g.::
+
+  #raw("data Nat = Z | S Nat", lang: "idris", block: true)

src/Parser/Unlit.idr

@@ -42,9 +42,16 @@ styleTeX = MkLitStyle
               Nil
               [".tex", ".ltx"]
 
+export
+styleTypst : LiterateStyle
+styleTypst = MkLitStyle
+               [("```idris", "```"), ("/* idris", "*/")]
+               Nil
+               [".typ"]
+
 
 supportedStyles : List LiterateStyle
-supportedStyles = [styleBird, styleOrg, styleCMark, styleTeX]
+supportedStyles = [styleBird, styleOrg, styleCMark, styleTeX, styleTypst]
 
 ||| Return the list of extensions used for literate files.
 export

tests/idris2/literate/literate019/Test1.typ

@@ -0,0 +1,15 @@
+= A test of literate Idris for typst
+
+/* idris
+silentlyDeclaredFunction : Nat -> Nat
+silentlyDeclaredFunction = (+6)
+*/
+
+Some text here
+
+== How, some visible code
+
+```idris
+f : Nat -> Nat
+f = (+8) . silentlyDeclaredFunction
+```

tests/idris2/literate/literate019/Test2.idr.typ

@@ -0,0 +1,32 @@
+/* idris
+module Test2
+*/
+
+= Another test, with extended extension
+
+/* idris
+silentlyDeclaredFunction' : Nat -> Nat
+silentlyDeclaredFunction' = (+6)
+*/
+
+Some text here
+
+== How, some visible code
+
+```idris
+f' : Nat -> Nat
+f' = (+8) . silentlyDeclaredFunction'
+```
+
+/* idris
+g' : Nat -> Nat
+g' = silentlyDeclaredFunction' . f'
+*/
+
+And now a hidden failing block:
+
+/* idris
+failing "ff"
+  h : Nat -> Nat
+  h = ff + 1
+*/

tests/idris2/literate/literate019/expected

@@ -0,0 +1,2 @@
+1/1: Building Test1 (Test1.typ)
+1/1: Building Test2 (Test2.idr.typ)

tests/idris2/literate/literate019/run

@@ -0,0 +1,4 @@
+. ../../../testutils.sh
+
+check Test1.typ
+check Test2.idr.typ