added low level rendering attributes (indent, spacing, ...)

diff --git a/helm/ocaml/cic_notation/renderingAttrs.ml b/helm/ocaml/cic_notation/renderingAttrs.ml
index fd2ddd24aa4747674d51ae71d2733d08a94c52bc..478ceff950e53d672996e91123c29eacdac7a864 100644 (file)
--- a/helm/ocaml/cic_notation/renderingAttrs.ml
+++ b/helm/ocaml/cic_notation/renderingAttrs.ml
@@ -42,3 +42,7 @@ let symbol_attributes _ = []
 let ident_attributes _ = []
 let number_attributes _ = []
 
+let spacing_attributes _ = [ None, "spacing", "0.5em" ]
+let indent_attributes _ = [ None, "indent", "0.5em" ]
+let small_skip_attributes _ = [ None, "width", "0.5em" ]
+

diff --git a/helm/ocaml/cic_notation/renderingAttrs.mli b/helm/ocaml/cic_notation/renderingAttrs.mli
index a9fc0badbc7cf86ef12c9b02a4e75426d1207429..64323598bce880deccea26ad7c9f3a0f2b99557c 100644 (file)
--- a/helm/ocaml/cic_notation/renderingAttrs.mli
+++ b/helm/ocaml/cic_notation/renderingAttrs.mli
@@ -29,6 +29,8 @@
 type xml_attribute = string option * string * string
 type markup = [ `MathML | `BoxML ]
 
+(** High-level attributes *)
+
 val keyword_attributes:                 (* let, match, in, ... *)
   markup -> xml_attribute list
 
@@ -47,3 +49,9 @@ val number_attributes:                  (* 1, 2, ... *)
 val object_keyword_attributes:          (* Body, Definition, ... *)
   markup -> xml_attribute list
 
+(** Low-level attributes *)
+
+val spacing_attributes: markup -> xml_attribute list
+val indent_attributes: markup -> xml_attribute list
+val small_skip_attributes: markup -> xml_attribute list
+