[ literate ] Support typst in literate Idris

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,17 +42,22 @@ styleTeX = MkLitStyle
               Nil
               [".tex", ".ltx"]
 
+export
+styleTypst : LiterateStyle
+styleTypst = MkLitStyle
+               [("```idris", "```"), ("/* idris", "*/")]
+               Nil
+               [".typ"]
+
+
+supportedStyles : List LiterateStyle
+supportedStyles = [styleBird, styleOrg, styleCMark, styleTeX, styleTypst]
 
 ||| Return the list of extensions used for literate files.
 export
 listOfExtensionsLiterate : List String
 listOfExtensionsLiterate
-  = do let exts = concatMap file_extensions
-              [ styleBird
-              , styleOrg
-              , styleCMark
-              , styleTeX
-              ]
+  = do let exts = concatMap file_extensions supportedStyles
        pfx <- [ "", ".idr", ".lidr"]
        ext <- exts
        pure (pfx ++ ext)
@@ -87,11 +92,7 @@ hasLitFileExt fname =
 ||| Are we dealing with a valid literate file name, if so return the identified style.
 export
 isLitFile : String -> Maybe LiterateStyle
-isLitFile fname
-    =   isStyle styleBird
-    <|> isStyle styleOrg
-    <|> isStyle styleCMark
-    <|> isStyle styleTeX
+isLitFile fname = choiceMap isStyle supportedStyles
 
   where
    hasSuffix : String -> Bool
@@ -116,11 +117,7 @@ isLitLine str
           _           => Nothing
 
     walk : Maybe (Maybe String, String)
-    walk
-      =   try styleBird
-      <|> try styleOrg
-      <|> try styleCMark
-      <|> try styleTeX
+    walk = choiceMap try supportedStyles
 
 export
 unlit : Maybe LiterateStyle -> String -> Either LiterateError String