X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=fe9b5f869b45fcd2e302e5b1f8a44863b5ac3a24;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hp=82a326c48bbb4ffc70d64400ef043b1b74955fa0;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/content_pres/cicNotationPres.ml b/matita/components/content_pres/cicNotationPres.ml
index 82a326c48..fe9b5f869 100644
--- a/matita/components/content_pres/cicNotationPres.ml
+++ b/matita/components/content_pres/cicNotationPres.ml
@@ -25,9 +25,7 @@
 
 (* $Id$ *)
 
-open Printf
-
-module Ast = CicNotationPt
+module Ast = NotationPt
 module Mpres = Mpresentation
 
 type mathml_markup = boxml_markup Mpres.mpres
@@ -102,7 +100,7 @@ let box_of mathonly spec attrs children =
 	let kind, spacing, indent = spec in
 	let dress children =
 	  if spacing then
-	    CicNotationUtil.dress small_skip children
+	    NotationUtil.dress small_skip children
 	  else
 	    children
 	in
@@ -194,20 +192,13 @@ 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 (UriManager.string_of_uri 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 use_unicode = true in *)
@@ -283,7 +274,7 @@ let render ~lookup_uri ?(prec=(-1)) =
             let substs' =
               box_of mathonly (A.H, false, false) []
                 (open_brace
-                :: (CicNotationUtil.dress semicolon
+                :: (NotationUtil.dress semicolon
                     (List.map
                       (fun (name, t) ->
                         box_of mathonly (A.H, false, false) [] [
@@ -299,7 +290,7 @@ let render ~lookup_uri ?(prec=(-1)) =
         let local_context l =
           box_of mathonly (A.H, false, false) []
             ([ Mpres.Mtext ([], "[") ] @ 
-            (CicNotationUtil.dress (Mpres.Mtext ([],  ";"))
+            (NotationUtil.dress (Mpres.Mtext ([],  ";"))
               (List.map 
                 (function 
                 | None -> Mpres.Mtext ([],  "_")
@@ -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: " ^ CicNotationPp.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
@@ -357,9 +348,9 @@ let render ~lookup_uri ?(prec=(-1)) =
               then ((*prerr_endline "reset";*)t')
               else add_parens child_prec prec t')
     in
-(*     prerr_endline (CicNotationPp.pp_term t); *)
+(*     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)
@@ -400,7 +391,7 @@ let render ~lookup_uri ?(prec=(-1)) =
     | A.Box ((_, spacing, _) as kind, terms) ->
         let children =
           aux_children mathonly spacing xref  prec
-            (CicNotationUtil.ungroup terms)
+            (NotationUtil.ungroup terms)
         in
         box_of mathonly kind attrs children
     | A.Mstyle (l,terms) -> 
@@ -408,19 +399,19 @@ let render ~lookup_uri ?(prec=(-1)) =
           (List.map (fun (k,v) -> None,k,v) l, 
            box_of mathonly (A.H, false, false) attrs 
             (aux_children mathonly false xref  prec 
-              (CicNotationUtil.ungroup terms)))
+              (NotationUtil.ungroup terms)))
     | A.Mpadded (l,terms) -> 
         Mpres.Mpadded 
           (List.map (fun (k,v) -> None,k,v) l, 
            box_of mathonly (A.H, false, false) attrs 
             (aux_children mathonly false xref  prec 
-              (CicNotationUtil.ungroup terms)))
+              (NotationUtil.ungroup terms)))
     | A.Maction alternatives -> 
          toggle_action (List.map invoke_reinit alternatives)
     | A.Group terms ->
 	let children =
           aux_children mathonly false xref  prec
-            (CicNotationUtil.ungroup terms)
+            (NotationUtil.ungroup terms)
         in
         box_of mathonly (A.H, false, false) attrs children
     | A.Break -> assert false (* TODO? *)