工作区

本指南涵盖 ReasLab 整体界面布局，介绍顶部栏、侧边栏、编辑器和信息面板如何协同工作，为您打造无缝的编辑体验。

界面总览

• 顶部导航栏：包含菜单按钮、打开的标签页（Tab）、当前文件及整个项目的在线协作人数，以及项目历史访问入口。
• 左侧工作面板：在目录树、全文搜索、语义搜索之间切换。
• 正中央编辑区：编写 Lean 代码与 Markdown 文档，支持撤销/重做、文件内查找、命令面板、符号面板等标准开发者体验。
• 右侧信息栏：针对 Lean 代码的 Infoview（即时目标/假设面板），或基于 Markdown 的实时渲染预览。

工作区布局

ReasLab 以若干核心面板为中心，实时同步您的每一次编辑：

顶部导航栏与标签页

• 项目菜单（Project Menu）：提供项目设置、成员管理、导出选项等全局操作。
• 标签页（Tabs）：点击标签切换文件，拖拽可调整顺序。
• 在线协作者（Online Peers）：显示当前文件及整体项目的在线人数，鼠标悬停可查看各协作者的光标位置。
• 项目历史（History）：浏览并恢复任意文件的历史快照。

左侧边栏

左侧边栏顶部有三个切换图标，分别对应三个功能面板：

• 文件（Files）— 分层目录树，支持新建/重命名/删除文件和文件夹，支持从桌面拖拽文件直接上传。
• 搜索（Search）— 在所有打开的文件中执行全文或正则表达式的搜索与替换。
• 语义搜索（Semantic）— 由 AI 驱动的语义理解搜索，能够理解数学语义而非仅做字面匹配。详细介绍见 Lean 指南。

正中央编辑器

• 工具栏位于编辑区上方，提供撤销/重做、注释切换、文件内搜索、命令面板和符号面板。
• 命令面板（Command Palette）：按 Cmd/Ctrl + K 唤出，输入关键词可快速筛选并执行数百种操作。
• 状态栏位于界面底部，显示当前模式（Lean 或 Markdown）、连接状态、光标位置以及当前激活的 Lean 工具链版本。

右侧信息栏

• Lean 文件自动打开 Infoview，实时展示证明目标（Goals）、已知假设（Hypotheses）和行内诊断信息。
• Markdown 文件呈现实时预览，编辑器与预览区同步滚动，编辑所见即所得。

文件资源管理器

左侧面板以清晰的目录树形式呈现项目结构，支持以下操作：

• 新建文件/文件夹：点击顶部的加号图标，在目录任意层级创建新文件或文件夹。
• 拖放上传：在浏览器内直接拖拽文件或文件夹以重新组织结构；也可从桌面将文件拖入文件树完成上传。
• 右键菜单：对任意文件或文件夹点击右键，可执行重命名、删除、复制、移动等操作。
• 图标区分：不同文件类型以不同图标显示 — Lean 文件、Markdown、图片、配置文件等一目了然。

文件历史与快照

每一次保存都会被自动追踪，您可以：

• 浏览历史：打开历史面板，查看任意文件的时间线改动记录，包含时间戳和操作者信息。
• 恢复历史版本：点击任意历史快照可预览其内容，确认后可一键恢复。
• 对比差异：在侧视图中对比当前文件与历史版本的差异，逐行高亮显示增删改内容。

全局文本搜索

侧边栏的 搜索（Search） 图标提供跨文件全文检索能力：

• 关键词搜索：输入任意关键词或短语，查找项目内所有匹配位置。
• 正则表达式：切换正则模式，以完整的正则表达式进行复杂模式匹配。
• 批量替换：在搜索面板中直接对所有匹配项执行「搜索+替换」，支持替换前预览变更。

搜索快捷键

快捷键	操作
Cmd/Ctrl + Shift + F	打开全局搜索
Enter	查找下一个匹配
Shift + Enter	查找上一个匹配
Cmd/Ctrl + Enter	替换当前匹配
Cmd/Ctrl + Shift + Enter	替换所有匹配

协作者在线状态

• 实时查看正在浏览同一文件的协作者 — 每个人的头像和光标位置均可见。
• 点击协作者面板可跳转到对应人员的光标位置。
• 多人同时编辑同一行时，以颜色区分的光标显示各自的编辑位置，互不冲突。