]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/content_pres/cicNotationPres.mli
Simplified rendering
[helm.git] / matitaB / components / content_pres / cicNotationPres.mli
index 57e7ee84463ee565399346248e19d8e75db9726c..65507f05394b7ba3a0a933de6f96244eedde15c3 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
-type mathml_markup = boxml_markup Mpresentation.mpres
-and boxml_markup = mathml_markup Box.box
 
-type markup = mathml_markup
+type markup = string Box.box
 
-(** {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
- * @param prec precedence level *)
 val render:
  #NCic.status ->
- lookup_uri:(Content.id -> string option) -> ?prec:int -> NotationPt.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 -> NotationPt.term -> Xml.token Stream.t *)
-
-val print_box:    boxml_markup -> Xml.token Stream.t
-val print_mpres:  mathml_markup -> Xml.token Stream.t
+ ?prec:int -> NotationPt.term ->
+   markup
 
+val render_sequent: 
+  #TermContentPres.status -> 
+  NotationPt.sequent ->
+    markup