-type entity = Section of id option (* section: Some id = open, None = close last *)
- | Global of bool * id * comm * term (* global entity: false = decl, true = def *)
+type command = Graph of id (* hierarchy graph: name *)
+ | Sorts of (int option * id) list (* sorts: index, name *)
+ | Section of id option (* section: Some id = open, None = close last *)
+ | Entity of kind * id * desc * term (* entity: class, name, description, contents *)