X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPres.mli;h=d0297387190ffd8bfd18ab40acccc59a7f9c7e39;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=3181ec0b8f5e1bb6caaeb9a94eca0fd19be5d102;hpb=256ea270b884864d0eddd1de66bae2a2cbc513ff;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPres.mli b/helm/ocaml/cic_notation/cicNotationPres.mli
index 3181ec0b8..d02973871 100644
--- a/helm/ocaml/cic_notation/cicNotationPres.mli
+++ b/helm/ocaml/cic_notation/cicNotationPres.mli
@@ -28,6 +28,25 @@ and boxml_markup = mathml_markup Box.box
 
 type markup = mathml_markup
 
-(** @param ids_to_uris mapping id -> uri for hyperlinking *)
+(** {2 Markup conversions} *)
+
+val mpres_of_box: boxml_markup -> mathml_markup
+val box_of_mpres: mathml_markup -> boxml_markup
+
+(** {2 Rendering} *)
+
+(** level 1 -> level 0
+ * @param ids_to_uris mapping id -> uri for hyperlinking *)
 val render: (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> markup
 
+(** level 0 -> xml stream *)
+val print_xml: markup -> Xml.token Stream.t
+
+(* |+* level 1 -> xml stream
+ * @param ids_to_uris +|
+val render_to_boxml:
+  (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> Xml.token Stream.t *)
+
+val print_box:    boxml_markup -> Xml.token Stream.t
+val print_mpres:  mathml_markup -> Xml.token Stream.t
+