fix admonition

Author: subfish-zhou

docs/assets/css/admonition-custom.css

@@ -1,58 +1,38 @@
-/* ---------- 通用变量（亮/暗配色可按需加[data-md-color-scheme]分支） ---------- */
 :root{
-  --admon-def-fg:   #1e88e5;  --admon-def-bg:   rgba(30,136,229,.08);
-  --admon-lemma-fg: #8e24aa;  --admon-lemma-bg: rgba(142,36,170,.08);
-  --admon-api-fg:   #00897b;  --admon-api-bg:   rgba(0,137,123,.08);
+  --admon-def-fg:#1e88e5;   --admon-def-bg:rgba(30,136,229,.08);
+  --admon-lemma-fg:#8e24aa; --admon-lemma-bg:rgba(142,36,170,.08);
+  --admon-api-fg:#00897b;   --admon-api-bg:rgba(0,137,123,.08);
 }
 
-/* ---------- 基础外观：圆角边框 + 内边距 ---------- */
+/* 容器：圆角 + 顶部留出角标空间 */
 .md-typeset .admonition.def,
 .md-typeset .admonition.lemma,
-.md-typeset .admonition.api,
-.md-typeset details.def,
-.md-typeset details.lemma,
-.md-typeset details.api{
-  position: relative;
-  border: 1px solid var(--md-default-fg-color--lighter);
-  border-radius: 12px;
-  padding: .6rem 1rem 1rem;
+.md-typeset .admonition.api{
+  position:relative; border:1px solid var(--md-default-fg-color--lighter);
+  border-radius:12px; padding:1.2rem 1rem 1rem; margin-top:1rem;
+  background:var(--md-default-bg-color);
 }
 
-/* ---------- 隐藏默认的标题与图标，防止“气泡”被遮挡 ---------- */
+/* 去掉默认小图标，避免挡住“胶囊” */
+.md-typeset .admonition.def   > .admonition-title::before,
+.md-typeset .admonition.lemma > .admonition-title::before,
+.md-typeset .admonition.api   > .admonition-title::before{ content:none; }
+
+/* 标题=左上角胶囊 */
 .md-typeset .admonition.def   > .admonition-title,
 .md-typeset .admonition.lemma > .admonition-title,
-.md-typeset .admonition.api   > .admonition-title{ display:none; }
-/*（若你还想保留原标题，仅隐藏图标，改成：.admonition-title::before{content:none;}）*/
-
-/* ---------- 左上“胶囊角标” ---------- */
-.md-typeset .admonition.def::before,
-.md-typeset .admonition.lemma::before,
-.md-typeset .admonition.api::before{
-  position: absolute; content: attr(data-label);
-  top: -12px; left: 16px; padding: .1rem .6rem;
-  border-radius: 999px; font-weight: 700; font-size: .85rem;
-  border: 1px solid;
-  background: var(--md-default-bg-color);
+.md-typeset .admonition.api   > .admonition-title{
+  position:absolute; top:-0.9rem; left:1rem; margin:0; padding:.1rem .6rem;
+  border-radius:999px; font-weight:700; font-size:.85rem;
+  background:var(--md-default-bg-color); border:1px solid currentColor;
 }
 
-/* 各类型配色（边框 & 胶囊前景/边框） */
-.md-typeset .admonition.def{
-  border-color: var(--admon-def-fg); box-shadow: 0 0 0 1px var(--admon-def-bg) inset;
-}
-.md-typeset .admonition.def::before{
-  color: var(--admon-def-fg); border-color: var(--admon-def-fg);
-}
+/* 配色 */
+.md-typeset .admonition.def{   border-color:var(--admon-def-fg);   box-shadow:0 0 0 1px var(--admon-def-bg) inset;}
+.md-typeset .admonition.def>.admonition-title{   color:var(--admon-def-fg); }
 
-.md-typeset .admonition.lemma{
-  border-color: var(--admon-lemma-fg); box-shadow: 0 0 0 1px var(--admon-lemma-bg) inset;
-}
-.md-typeset .admonition.lemma::before{
-  color: var(--admon-lemma-fg); border-color: var(--admon-lemma-fg);
-}
+.md-typeset .admonition.lemma{ border-color:var(--admon-lemma-fg); box-shadow:0 0 0 1px var(--admon-lemma-bg) inset;}
+.md-typeset .admonition.lemma>.admonition-title{ color:var(--admon-lemma-fg); }
 
-.md-typeset .admonition.api{
-  border-color: var(--admon-api-fg); box-shadow: 0 0 0 1px var(--admon-api-bg) inset;
-}
-.md-typeset .admonition.api::before{
-  color: var(--admon-api-fg); border-color: var(--admon-api-fg);
-}
+.md-typeset .admonition.api{   border-color:var(--admon-api-fg);   box-shadow:0 0 0 1px var(--admon-api-bg) inset;}
+.md-typeset .admonition.api>.admonition-title{   color:var(--admon-api-fg); }

docs/projects/verso.md

@@ -12,31 +12,27 @@ Verso 是用于撰写 Lean 文档的构建框架+具体工具。 你可以使用
 - 网页
 - 学术论文
 
-它能够显示 Lean 代码、提供测试以避免文档年久失修、提供超链接等。它能够支持线性或链接错综的文档结构，提供交互，以及导出PDF。
+它能够显示 Lean 代码、提供测试以避免文档年久失修、提供超链接等。它能够支持线性或交叉引用错综的文档结构，提供交互，以及导出PDF。
 
 Verso由以下组件构成：
 
 **标记语言** 一种 Markdown 的简化变体，同时是 Lean 本身的另一种具体语法，因此 Verso 文档也是 Lean 文件。正如 TeX、Sphinx 和 Scribble 允许使用自己的编程语言扩展他们的语言一样，Verso 的标记语言是可扩展的。你可以在文件顶部定义一个 Lean 函数，随后在该文件的文本中使用它。
 
 **可扩展的文档结构** 所有 Verso 文档都可以包含一组通用元素，例如段落、强调文本或图像。 它们还共享部分和子部分的分层结构。 这些类型可按各个体裁进行扩展。
 
-阐述和渲染框架
-Verso为作者提供的文本转换至可读输出建立了一套共享范式。不同体裁将生成不同的输出格式，但无需重复实现交叉引用解析功能，并能受益于共享库实现多格式输出。
+**阐释（Elaboration）和渲染框架** Verso为作者提供的文本转换至可读输出建立了一套共享范式。不同体裁将生成不同的输出格式，但无需重复实现交叉引用解析功能，并能受益于共享库实现多格式输出。
 
-【交叉引用管理】
-Verso包含：用于表示文档化项目的通用范式，以及在HTML输出体裁间共享交叉引用数据库的格式。这使得链接与交叉引用能够自动插入和维护。
+**交叉引用管理** Verso包含：用于表示文档化项目的通用范式，以及在HTML输出体裁间共享交叉引用数据库的格式。这使得链接与交叉引用能够自动插入和维护。
 
-【Lean代码渲染】
-Verso具备阐释和展示文档中Lean代码的功能。在HTML输出中，该代码呈现为可切换的证明状态、悬停提示和超链接形式。得益于精准的语法高亮（基于正则表达式的方法因Lean语法可扩展性而无法实现），代码显示更加清晰。
+**Lean代码渲染** Verso具备阐释和展示文档中Lean代码的功能。在HTML输出中，该代码呈现为可切换的证明状态、悬停提示和超链接形式。得益于精准的语法高亮（基于正则表达式的方法因Lean语法可扩展性而无法实现），代码显示更加清晰。
 
 通过SubVerso辅助库，Verso文档可处理自Lean 4.0.0起任何版本的Lean代码。这使文档能够进行版本对比分析，并实现项目所用Lean版本与说明文档所用Lean版本的解耦升级。
 
-【工具库】
-Verso包含可供各体裁使用的工具库，提供诸如HTML内容全文检索等功能。这些库无需额外构建时依赖，避免了同时维护多个库生态系统带来的复杂性。
+**工具库** Verso包含可供各体裁使用的工具库，提供诸如HTML内容全文检索等功能。这些库无需额外构建时依赖，避免了同时维护多个库生态系统带来的复杂性。
 
 ## 体裁
 
-!!! def "" {data-label="def"}
+!!! def "def"
     ```lean
     List.forM {u v w} {m : Type u → Type v} [Monad m]
     {a : Type w} (as : List a) (f : a → m PUnit) : m PUnit
@@ -49,6 +45,13 @@ Verso包含可供各体裁使用的工具库，提供诸如HTML内容全文检
 
     参见：`List.mapM`（收集结果的变体）。
 
+!!! lemma "lemma"
+    这里是一个引理块的示例。
+
+!!! api "API"
+    这里是 API 描述块的示例。
+
+
 ## Verso 标记语言
 
 ## 构建文档

mkdocs.yml

@@ -20,7 +20,6 @@ theme:
     - search.share
     - content.code.copy
     - content.code.annotate
-    - content.tooltips
 
 plugins:
   - search:
@@ -54,6 +53,7 @@ markdown_extensions:
       custom_checkbox: true
   - pymdownx.tilde
   - def_list
+  - attr_list
 
 extra_javascript:
   - https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.0/MathJax.js?config=TeX-AMS-MML_HTMLorMML