/-!
# RichContent —— 富内容(ADR-0006 的 prose 母本)

ADR-0006:element schema 的"叶子"可以是 `content` 类型,其值是**一段 typst 源**,
语义取该源作为 module 求值后的 body content。关键约束(均 ADR-0006,源自 typst 源码
事实):富内容**不可无主**——typst 的源必须有 `FileId`,否则 span 脱锚、相对 import
报"cannot access file system from here"。故每段富内容是 World 里的一等文件,坐落在
一个**虚拟路径**上;相对 import 限本工程路径结构内 + `@package`(不跨工程)。

本模块只立 prose 锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON
Schema 形状属实现细节,不进 Lean,只承诺"富内容由一个虚拟路径定位"这一条关系。
-/

namespace Spec.Courseware

/-- 富内容在工程文件路径结构中的**虚拟路径**(`OPEN` 表示, ADR-0006)。把一段富内容
定位为 World 里的一等文件(span 可解析、相对 import 可锚定)。落盘后即真实相对路径
(ADR-0007),不在本层承诺,故 opaque。 -/
opaque VPath : Type

/-- 对一段富内容的**引用**:它坐落在某个虚拟路径上(`PINNED` 关系, ADR-0006)。
刻意**不**建模源文本、不建模求值出的 `Content`(那是实现侧的事);只钉"富内容经由一个
`VPath` 定位",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/
structure RichContentRef where
  /-- 该富内容所在的虚拟路径(ADR-0006;落盘后为真实相对路径, ADR-0007)。 -/
  vpath : VPath

end Spec.Courseware