Markdown 编辑与预览

ReasLab 支持在项目中编写和预览 Markdown 文档。您可以用 Markdown 记录项目说明、定理与证明思路、实验结果，或编写包含数学公式、Lean 代码和图表的研究文档。

快速开始

1. 在项目中创建或打开一个 .md 文件。
2. 点击编辑器工具栏中的眼睛图标（Toggle Markdown Preview）。
3. 在编辑器右侧查看实时渲染结果。
4. 如需更大的阅读区域，点击预览区右上角的 Full View。

Markdown 预览默认关闭。ReasLab 会按项目记住预览的开关状态，再次进入同一项目时沿用上一次的设置。打开 .md 文件后，编辑器底部状态栏会显示 Markdown 模式。

Markdown 基础语法

下面的示例涵盖常用 Markdown 写法：

# 一级标题
## 二级标题

这是 **粗体**、*斜体* 和 ~~删除线~~。

- 无序列表
- 第二项

1. 有序列表
2. 第二项

> 这是一段引用。

[ReasLab](https://reaslab.io)

`inline code`

ReasLab 还支持 GitHub Flavored Markdown（GFM）中的表格、任务列表、删除线和自动链接。例如：

| 模块 | 状态 |
| --- | --- |
| 定理说明 | 完成 |
| Lean 证明 | 进行中 |

- [x] 整理定理陈述
- [ ] 完成形式化证明

如果您不熟悉 Markdown，可以阅读 GitHub Markdown 基础语法。本指南后续重点介绍 ReasLab 提供的编辑、预览和数学写作能力。

文档大纲

打开 .md 文件后，左侧 Explore 面板下方的 OUTLINE 会根据标题生成文档大纲。

• # 至 ###### 标题会按照级别组成树形结构；Setext 风格的一、二级标题也会显示。
• 光标移动到某一章节时，对应的大纲项会自动高亮。
• 点击大纲项可跳转到编辑器中的对应标题。
• 点击节点前的箭头可展开或折叠其子标题。
• 使用大纲标题栏右侧的按钮可以全部折叠或全部展开。
• 拖动文件树与大纲之间的分隔线可以调整高度；点击 OUTLINE 标题栏可以收起或展开整个大纲区域。

合理使用标题层级可以让较长的研究笔记、证明说明和项目文档更容易浏览。

实时预览

Markdown 源码和渲染结果以左右分栏方式显示。编辑内容后，预览会自动更新，无需手动刷新。

开启或关闭预览

点击编辑器工具栏中的眼睛图标即可打开或关闭预览。该设置按项目保存，因此不同项目可以保留各自的布局。

双向同步滚动

编辑器与预览区支持双向同步滚动：滚动源码时，预览会跟随到对应内容；滚动预览时，编辑器也会定位到相应行。对于包含长公式、代码块或多个章节的文档，这有助于保持两侧上下文一致。

Full View

点击预览区右上角的最大化按钮，可在 Markdown Preview 窗口中查看接近全屏的渲染结果。关闭窗口后可以继续在分栏模式中编辑。

数学公式

ReasLab 使用 KaTeX 渲染常用的 LaTeX 数学语法，同时支持美元符号和括号两组分隔符。

行内公式

函数 $f(x)=x^2$ 在 \(x=0\) 处取得最小值。

块级公式

$$
\min_x f(x) \quad \text{s.t.} \quad Ax=b
$$

\[
\sum_{i=1}^{n} x_i = 1
\]

公式分隔符必须成对出现。转义后的美元符号、未闭合的分隔符，以及行内代码或围栏代码块中的 $ 不会被渲染为公式。需要查询具体命令是否受支持时，请参考 KaTeX 支持的函数列表。KaTeX 面向数学公式渲染，并不支持完整的 LaTeX 文档、宏包和排版流程。

代码块

在围栏代码块起始位置写入语言标识符，即可启用对应的语法高亮：

```python
def square(x):
    return x * x
```

```json
{"status": "ok"}
```

预览中的代码块支持复制和下载。代码块只用于展示，不会在 Markdown 预览中执行。

Lean 代码块

使用 lean 或 lean4 标识符可启用专门的 Lean 高亮：

```lean
theorem add_zero (n : Nat) : n + 0 = n := by
  simp
```

Lean 代码块支持明暗主题语法高亮和彩虹括号；不匹配的括号会以不同颜色提示。

Mermaid 图表

使用 mermaid 围栏代码块，可以在预览中渲染流程图等结构化图表：

```mermaid
flowchart LR
  A[编写 Markdown] --> B[实时预览]
  B --> C[完善文档]
```

渲染后的 Mermaid 图表提供复制源码、下载图表、全屏查看和缩放控制。如果图表无法渲染，请先检查 Mermaid 语法以及代码块的语言标识符是否正确。

图片与链接

项目内图片

Markdown 可以引用项目中已经存在的图片。相对路径以当前 .md 文件所在目录为基准：

![实验结果](./images/result.png)
![上级目录中的模型图](../assets/model.png)

建议始终填写有意义的替代文本，以便在图片无法加载时说明其内容。路径和文件名区分大小写；如果预览显示图片不可用，请检查图片是否已经存在于项目中，以及相对路径是否正确。

远程图片与网页链接

可以通过 HTTP(S) 地址引用远程图片或网页：

![远程图片](https://example.com/image.png)
[访问相关资料](https://example.com)

远程资源能否显示还取决于资源地址是否有效，以及对方服务器的访问策略。系统或 AI 输出中指向当前工作区可见文件的链接，可以直接在 ReasLab 标签页中打开；无效、不可见或属于其他项目的文件链接会被阻止。

典型使用场景

• 项目说明：使用 README.md 记录目录结构、运行方式和协作约定。
• 定理与证明笔记：先用自然语言和公式整理命题，再逐步转写为 Lean。
• 代码说明：在同一文档中组合算法描述、Lean/Python 代码和运行结果。
• 研究与建模文档：使用标题、公式、表格、任务列表和 Mermaid 图表组织研究过程。
• 团队协作：将背景材料、决策记录和后续任务保存在项目中，与代码共同维护。

支持范围与常见问题

为什么没有出现 Markdown 预览？

确认当前文件使用 .md 扩展名，然后点击编辑器工具栏中的眼睛图标。预览默认不会自动打开。

为什么公式没有渲染？

检查分隔符是否成对闭合，并确认公式使用的是 KaTeX 支持的命令。完整 LaTeX 文档、宏包加载、参考文献和交叉引用不属于 Markdown 公式预览能力。

为什么图片无法显示？

确认文件已经存在于项目中，并从当前 .md 文件所在目录重新检查相对路径和文件名大小写。远程图片还可能受到网络或来源服务器限制。

为什么代码没有运行？

Markdown 代码块仅提供展示、语法高亮、复制和下载，不负责执行代码。需要运行 Python 或验证 Lean 代码时，请在对应的源文件中操作。

HTML 和其他扩展语法是否都受支持？

ReasLab 会对 Markdown 中的 HTML 进行安全过滤，因此不保证任意 HTML 标签、属性或脚本原样渲染。脚注等非 GFM 扩展也不属于当前明确支持的范围。

相关指南

• 工作区：了解编辑器、文件树和侧边栏布局。
• Lean 工具链支撑：编写和验证 Lean 代码。
• Lean 形式化：将自然语言、Markdown 或 LaTeX 命题转写为 Lean。
• LaTeX 编辑与 PDF 预览：编写和编译完整 LaTeX 文档。