]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/content_pres/cicNotationPres.ml
Use of standard OCaml syntax
[helm.git] / matita / components / content_pres / cicNotationPres.ml
index 5f9f202caeaf09b8d7b299444018106abe8a6062..0602548a10039b6bcced4e07f9ac9b80b0302d36 100644 (file)
@@ -25,8 +25,6 @@
 
 (* $Id$ *)
 
-open Printf
-
 module Ast = NotationPt
 module Mpres = Mpresentation
 
@@ -194,22 +192,15 @@ let add_parens child_prec curr_prec t =
     match t with
     | Mpresentation.Mobject (_, box) ->
         mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ]))
-    | mpres -> Mpresentation.Mrow ([], [open_paren; t; closed_paren])
+    | _mpres -> Mpresentation.Mrow ([], [open_paren; t; closed_paren])
   end else
     ((*prerr_endline ("NOT adding parens around: "^
       BoxPp.render_to_string (function x::_->x|_->assert false)
         ~map_unicode_to_tex:false 80 t);*)t)
 
-let lookup_uri ids_to_uris id =
- try
-   let uri = Hashtbl.find ids_to_uris id in
-   Some (NReference.string_of_reference uri)
- with Not_found -> None
-;;
-
-let render ~lookup_uri ?(prec=(-1)) =
+let render status ~lookup_uri ?(prec=(-1)) =
   let module A = Ast in
-  let module P = Mpresentation in
+  (*let module P = Mpresentation in*)
 (*   let use_unicode = true in *)
   let make_href xmlattrs xref =
     let xref_uris =
@@ -316,9 +307,9 @@ let render ~lookup_uri ?(prec=(-1)) =
     | A.Magic _
     | A.Variable _ -> assert false  (* should have been instantiated *)
     | t ->
-        prerr_endline ("unexpected ast: " ^ NotationPp.pp_term t);
+        prerr_endline ("unexpected ast: " ^ NotationPp.pp_term status t);
         assert false
-  and aux_attributes xmlattrs mathonly xref  prec t =
+  and aux_attributes _xmlattrs mathonly _xref  prec t =
     let reset = ref false in
     let inferred_level = ref None in
     let expected_level = ref None in
@@ -359,7 +350,7 @@ let render ~lookup_uri ?(prec=(-1)) =
     in
 (*     prerr_endline (NotationPp.pp_term t); *)
     aux_attribute t
-  and aux_literal xmlattrs xref prec l =
+  and aux_literal xmlattrs xref _prec l =
     let attrs = make_href xmlattrs xref in
     (match l with
     | `Symbol s -> Mpres.Mo (attrs, to_unicode s)