Skip to content

Commit d58567c

Browse files
committed
test admonition block
1 parent dd92209 commit d58567c

File tree

4 files changed

+75
-18
lines changed

4 files changed

+75
-18
lines changed
Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
/* ---------- 通用变量(亮/暗配色可按需加[data-md-color-scheme]分支) ---------- */
2+
:root{
3+
--admon-def-fg: #1e88e5; --admon-def-bg: rgba(30,136,229,.08);
4+
--admon-lemma-fg: #8e24aa; --admon-lemma-bg: rgba(142,36,170,.08);
5+
--admon-api-fg: #00897b; --admon-api-bg: rgba(0,137,123,.08);
6+
}
7+
8+
/* ---------- 基础外观:圆角边框 + 内边距 ---------- */
9+
.md-typeset .admonition.def,
10+
.md-typeset .admonition.lemma,
11+
.md-typeset .admonition.api,
12+
.md-typeset details.def,
13+
.md-typeset details.lemma,
14+
.md-typeset details.api{
15+
position: relative;
16+
border: 1px solid var(--md-default-fg-color--lighter);
17+
border-radius: 12px;
18+
padding: .6rem 1rem 1rem;
19+
}
20+
21+
/* ---------- 隐藏默认的标题与图标,防止“气泡”被遮挡 ---------- */
22+
.md-typeset .admonition.def > .admonition-title,
23+
.md-typeset .admonition.lemma > .admonition-title,
24+
.md-typeset .admonition.api > .admonition-title{ display:none; }
25+
/*(若你还想保留原标题,仅隐藏图标,改成:.admonition-title::before{content:none;})*/
26+
27+
/* ---------- 左上“胶囊角标” ---------- */
28+
.md-typeset .admonition.def::before,
29+
.md-typeset .admonition.lemma::before,
30+
.md-typeset .admonition.api::before{
31+
position: absolute; content: attr(data-label);
32+
top: -12px; left: 16px; padding: .1rem .6rem;
33+
border-radius: 999px; font-weight: 700; font-size: .85rem;
34+
border: 1px solid;
35+
background: var(--md-default-bg-color);
36+
}
37+
38+
/* 各类型配色(边框 & 胶囊前景/边框) */
39+
.md-typeset .admonition.def{
40+
border-color: var(--admon-def-fg); box-shadow: 0 0 0 1px var(--admon-def-bg) inset;
41+
}
42+
.md-typeset .admonition.def::before{
43+
color: var(--admon-def-fg); border-color: var(--admon-def-fg);
44+
}
45+
46+
.md-typeset .admonition.lemma{
47+
border-color: var(--admon-lemma-fg); box-shadow: 0 0 0 1px var(--admon-lemma-bg) inset;
48+
}
49+
.md-typeset .admonition.lemma::before{
50+
color: var(--admon-lemma-fg); border-color: var(--admon-lemma-fg);
51+
}
52+
53+
.md-typeset .admonition.api{
54+
border-color: var(--admon-api-fg); box-shadow: 0 0 0 1px var(--admon-api-bg) inset;
55+
}
56+
.md-typeset .admonition.api::before{
57+
color: var(--admon-api-fg); border-color: var(--admon-api-fg);
58+
}

docs/assets/css/admonition-def.css

Lines changed: 0 additions & 9 deletions
This file was deleted.

docs/projects/verso.md

Lines changed: 16 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -18,27 +18,36 @@ Verso由以下组件构成:
1818

1919
**标记语言** 一种 Markdown 的简化变体,同时是 Lean 本身的另一种具体语法,因此 Verso 文档也是 Lean 文件。正如 TeX、Sphinx 和 Scribble 允许使用自己的编程语言扩展他们的语言一样,Verso 的标记语言是可扩展的。你可以在文件顶部定义一个 Lean 函数,随后在该文件的文本中使用它。
2020

21-
**可扩展的文档结构** 所有 Verso 文档都可以包含一组通用元素,例如段落、强调文本或图像。 它们还共享部分和子部分的分层结构。 这些类型可按各个流派进行扩展
21+
**可扩展的文档结构** 所有 Verso 文档都可以包含一组通用元素,例如段落、强调文本或图像。 它们还共享部分和子部分的分层结构。 这些类型可按各个体裁进行扩展
2222

2323
阐述和渲染框架
24-
Verso 提供了一种共享范例,用于将作者编写的文本转换为可读的输出。 不同的流派会产生不同的输出格式,但它们不需要重新发明轮子来解决交叉引用问题,并且它们可以从共享库中受益,以生成各种格式的输出
24+
Verso为作者提供的文本转换至可读输出建立了一套共享范式。不同体裁将生成不同的输出格式,但无需重复实现交叉引用解析功能,并能受益于共享库实现多格式输出
2525

26+
【交叉引用管理】
27+
Verso包含:用于表示文档化项目的通用范式,以及在HTML输出体裁间共享交叉引用数据库的格式。这使得链接与交叉引用能够自动插入和维护。
2628

27-
## 流派
29+
【Lean代码渲染】
30+
Verso具备阐释和展示文档中Lean代码的功能。在HTML输出中,该代码呈现为可切换的证明状态、悬停提示和超链接形式。得益于精准的语法高亮(基于正则表达式的方法因Lean语法可扩展性而无法实现),代码显示更加清晰。
2831

29-
!!! note "def"
32+
通过SubVerso辅助库,Verso文档可处理自Lean 4.0.0起任何版本的Lean代码。这使文档能够进行版本对比分析,并实现项目所用Lean版本与说明文档所用Lean版本的解耦升级。
33+
34+
【工具库】
35+
Verso包含可供各体裁使用的工具库,提供诸如HTML内容全文检索等功能。这些库无需额外构建时依赖,避免了同时维护多个库生态系统带来的复杂性。
36+
37+
## 体裁
38+
39+
!!! def "" {data-label="def"}
3040
```lean
3141
List.forM {u v w} {m : Type u → Type v} [Monad m]
3242
{a : Type w} (as : List a) (f : a → m PUnit) : m PUnit
3343
```
34-
3544
Applies the monadic action `f` to every element in the list, in order.
3645

3746
参数说明:
38-
: **as** — 输入列表
47+
: **as** — 输入列表
3948
: **f** — 作用在元素上的 monadic 函数
4049

41-
参见:`List.mapM`(收集结果的变体)。
50+
参见:`List.mapM`(收集结果的变体)。
4251

4352
## Verso 标记语言
4453

mkdocs.yml

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,13 +54,12 @@ markdown_extensions:
5454
custom_checkbox: true
5555
- pymdownx.tilde
5656
- def_list
57-
- attr_list
5857

5958
extra_javascript:
6059
- https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.0/MathJax.js?config=TeX-AMS-MML_HTMLorMML
6160

6261
extra_css:
63-
- assets/css/admonition-def.css
62+
- assets/css/admonition-custom.css
6463
- assets/css/custom.css
6564
- https://cdnjs.cloudflare.com/ajax/libs/font-awesome/5.15.4/css/all.min.css
6665

0 commit comments

Comments
 (0)