@aufbau/editor

MM0理论和Aufbau证明的可嵌入浏览器编辑器组件. 汇编和诊断在WebAssembly在当地进行.

安装

npm install @aufbau/editor @aufbau/compiler \
  @codemirror/view @codemirror/state @codemirror/commands \
  @codemirror/lint

对于语言服务器徘徊、完成和验证搜索,也安装 可选软件包 :

npm install @aufbau/lsp @codemirror/autocomplete

使用量

导入包时登记其自定义元素 :

import "@aufbau/editor";

<aufbau-theory id="example" src="/example.mm0"></aufbau-theory>

<aufbau-proof theory="example" src="/example.auf"></aufbau-proof>

来源也可能是内含的:

<aufbau-theory id="example">
  <script type="text/mm0">
    -- MM0 source
  </script>
</aufbau-theory>

<aufbau-proof theory="example">
  <script type="text/auf">
    -- Aufbau proof script
  </script>
</aufbau-proof>

具有相同特性的多个证明要素 theory 值在 DOM 中形成一个文档 秩序。 秩序。 使用 readonly, (中文(简体) ), theme="light|dark|auto",或 lsp="off" 调整一个 个人证明要素。 该软件包还登记 <aufbau-index> (单位:千美元) 现场语句索引.

理论和证据可能 import "other.mm0"; 编号 : include "other.auf";编辑 已命名文件相对于页面( 内入源) 或源文件 拥有 URL (src 来源),并获取 .mm0 带上它 .auf 一起来 当服务器有一个.

此软件包需要浏览器 DOM. 它不运行在平地节点下.

从 CDN 装入

组件不需要捆绑,也不需要建设步骤——导入地图就够了。 这个 ?external= 参数将 CodeMirror 和 Aufbau 主题包保持为单一 共享实例而不是每个依赖者一份副本 :

<script type="importmap">
  {
    "imports": {
      "@codemirror/state": "https://esm.sh/@codemirror/state",
      "@codemirror/view": "https://esm.sh/@codemirror/view?external=@codemirror/state",
      "@codemirror/commands": "https://esm.sh/@codemirror/commands?external=@codemirror/state,@codemirror/view",
      "@codemirror/lint": "https://esm.sh/@codemirror/lint?external=@codemirror/state,@codemirror/view",
      "@codemirror/autocomplete": "https://esm.sh/@codemirror/autocomplete?external=@codemirror/state,@codemirror/view",
      "@aufbau/compiler": "https://esm.sh/@aufbau/compiler",
      "@aufbau/lsp": "https://esm.sh/@aufbau/lsp",
      "@aufbau/editor": "https://esm.sh/@aufbau/editor?external=@aufbau/compiler,@aufbau/lsp,@codemirror/state,@codemirror/view,@codemirror/commands,@codemirror/lint,@codemirror/autocomplete"
    }
  }
</script>
<script type="module">
  import "@aufbau/editor";
</script>

语言服务器在 Web Worker 中运行,浏览器只能从中构建 一个同源的脚本,所以 @aufbau/lsp 靴子绑住它 blob: URL 当 它从一个CDN服务。 因此,需要一个内容-安全政策的网页 worker-src blob: 与CDN主机一起 @aufbau/lsp 读取。 丢弃 页:1 @aufbau/lsp 财务报告和审定财务报表 @codemirror/autocomplete 不包含要运行的条目 语言服务器;编辑器仍会编译并报告诊断.

拥有自己全球键盘快捷键的主机页面应注意 键键键在细胞泡中被打出其阴影根,重新瞄准 <aufbau-*> 主机元素 。 如果这些快捷键吞下普通字符,请停止 键盘事件 composedPath() 包含一个 AUFBAU- 元素在 页面的处理者看到他们.