From 1d20c8204a6f7340dcf71702c02d5b6b53311ed4 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Sat, 26 Oct 2024 21:13:38 +0300 Subject: [PATCH 1/2] [ refactor ] Do not repeat list of supported styles --- src/Parser/Unlit.idr | 22 ++++++---------------- 1 file changed, 6 insertions(+), 16 deletions(-) diff --git a/src/Parser/Unlit.idr b/src/Parser/Unlit.idr index afd157d100..66ee418b7b 100644 --- a/src/Parser/Unlit.idr +++ b/src/Parser/Unlit.idr @@ -43,16 +43,14 @@ styleTeX = MkLitStyle [".tex", ".ltx"] +supportedStyles : List LiterateStyle +supportedStyles = [styleBird, styleOrg, styleCMark, styleTeX] + ||| 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 +85,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 +110,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 From 947d014c52c76b0c47bde9a25ad2ef39744e447d Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Sat, 26 Oct 2024 21:10:00 +0300 Subject: [PATCH 2/2] [ literate ] Add support for typst files --- CHANGELOG_NEXT.md | 2 + docs/source/reference/literate.rst | 70 ++++++++++++++++++++++++++++-- src/Parser/Unlit.idr | 9 +++- 3 files changed, 77 insertions(+), 4 deletions(-) diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 2cb67aff00..e3322e182e 100644 --- a/CHANGELOG_NEXT.md +++ b/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 diff --git a/docs/source/reference/literate.rst b/docs/source/reference/literate.rst index 67f0746909..92cdccd30a 100644 --- a/docs/source/reference/literate.rst +++ b/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 ` would also be welcome. +But more importantly, a more intelligent processing of literate documents using a pandoc like library in Idris such as: +`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 ```` are treated as invisible code blocks:: ++ Comment blocks of the form ```` are treated as invisible code blocks:: ++ Syntax of beginnings and endings of visible and invisible code blocks must not have preceding white spaces:: + + Some text + + ```idris + -- treated as visible code + ``` + + + + - Some list element + + ```idris + -- code here will be ignored by the compiler + ``` + + + + 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 `_ 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) diff --git a/src/Parser/Unlit.idr b/src/Parser/Unlit.idr index 66ee418b7b..0581e620bd 100644 --- a/src/Parser/Unlit.idr +++ b/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