文学编程（Literate Programming）

Idris2 支持多种文学编程模式风格。

unlit 设计时假定正在解析类似 markdown 的语言。unlit 由词法分析器（Lexer）根据指定的文学风格识别代码块和代码行，其他内容会被忽略。Idris2 还支持利用各文学风格的"原生特性"识别"可见"和"不可见"代码块。

一种文学风格包括：

一组字符串形式的代码块分隔符；
一组行标记符；
一组有效的文件扩展名。

词法分析采用简单且贪婪的方式：一旦进入代码块，直到遇到结束分隔符前，所有内容都视为代码。这意味着在文学文件中使用 verbatim 模式也会被视为活跃代码。

未来应支持文学 LaTeX 文件及其他常见文档格式。更重要的是，欢迎在 Idris 中用类似 pandoc 的库（如 Edda）对文学文档进行更智能的处理。

Bird 风格文学文件（Bird Style Literate Files）

扩展名为 .lidr 的文件被视为 Bird 风格文学文件。

Bird 记号是一种经典的文学编程模式，见于 Haskell（和 Orwell），其中可见代码行以 > 开头，隐藏行以 < 开头，其他行视为文档。

备注

我们与传统 lhs2tex 有所不同，后者用 < 显示非活跃代码。Bird 风格按原样呈现，建议使用其他风格以获得更全面的文学编程体验。

嵌入到类 Markdown 文档中（Embedding in Markdown-like documents）

虽然 Bird 风格文学模式很有用，但不太适合现代的 markdown 类标记（如 Org-Mode 和 CommonMark）。Idris2 也支持在 CommonMark 和 OrgMode 文档中用原生代码块和代码行识别"可见"和"不可见"代码块及行。

其理念如下：

**可见**内容会保留在美化输出中；
**不可见**内容会被移除；
**规范**内容会原样显示，不被编译器处理。

OrgMode

扩展名为 .org 的文件被视为 Org 风格文学文件。下列标记均可识别（不区分大小写）：

Org mode 中不带选项的 idris 源代码块会被识别为可见代码块：
```
#+begin_src idris
data Nat = Z | S Nat
#+end_src
```
以 #+BEGIN_COMMENT idris 开头的注释块会被视为不可见代码块：
```
#+begin_comment idris
data Nat = Z | S Nat
#+end_comment
```
不支持可见代码行和规范。不可见代码行用 #+IDRIS: 标记：
```
#+IDRIS: data Nat = Z | S Nat
```

规范内容可用 OrgMode 的普通源代码块或示例块表示：

#+begin_src
map : (f : a -> b)
   -> List a
   -> List b
map f _ = Nil
#+end_src

CommonMark

扩展名为 .md 或 .markdown 的 Markdown 文件，以及扩展名为 .dj 的 Djot 文件，被视为 CommonMark 风格文学文件。

CommonMark 中不带选项的 idris 源代码块会被识别为可见代码块：
```
```idris
data Nat = Z | S Nat
```

~~~idris
data Nat = Z | S Nat
~~~
```
Comment blocks of the form  are treated as invisible code blocks:
```

```

可见和不可见代码块的起止语法前不能有空白字符：

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

不支持代码行。

规范内容可用 CommonMark 的预格式化块（缩进四个空格）或无标签代码块表示：

Compare

```idris
map : (f : a -> b)
   -> List a
   -> List b
map f _ = Nil
```

with

    map : (f : a -> b)
       -> List a
       -> List b
    map f _ = Nil

LaTeX

扩展名为 .tex 和 .ltx 的文件被视为 LaTeX 风格文学文件。

名为 code 的环境会被视为可见代码块：

\begin{code}
data Nat = Z | S Nat
\end{code}

名为 hidden 的环境会被视为不可见代码块：

\begin{hidden}
data Nat = Z | S Nat
\end{hidden}

不支持代码行。
规范内容可用用户自定义环境表示。

我们不为这些代码块提供定义，需用户自行定义。例如可用 fancyverbatim 和 comment 宏包：

\usepackage{fancyvrb}
\DefineVerbatimEnvironment
  {code}{Verbatim}
  {}

\usepackage{comment}

\excludecomment{hidden}

Typst

扩展名为 .typ 的文件被视为 Typst 风格文学文件。

设置为 Idris 语言的代码块会被识别为可见代码块：
```
```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
*/
```

可见和不可见代码块的起止语法前不能有空白字符：

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
  */

不支持用 #raw 函数的代码行。
规范内容可用 #raw 函数并设置语言和块来表示，例如：
```
#raw("data Nat = Z | S Nat", lang: "idris", block: true)
```