- disk dumping of ex-lexicon commands almost implemented

[helm.git] / matita / components / content_pres / cicNotationPres.ml

diff --git a/matita/components/content_pres/cicNotationPres.ml b/matita/components/content_pres/cicNotationPres.ml
index 82a326c48bbb4ffc70d64400ef043b1b74955fa0..d3465d30a4e21d46b903f70ac0afa67df7c6990f 100644 (file)
--- a/matita/components/content_pres/cicNotationPres.ml
+++ b/matita/components/content_pres/cicNotationPres.ml
@@ -27,7 +27,7 @@
 
 open Printf
 
-module Ast = CicNotationPt
+module Ast = NotationPt
 module Mpres = Mpresentation
 
 type mathml_markup = boxml_markup Mpres.mpres
@@ -102,7 +102,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
@@ -200,13 +200,6 @@ let add_parens child_prec curr_prec t =
       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 module A = Ast in
   let module P = Mpresentation in
@@ -283,7 +276,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 +292,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,7 +309,7 @@ 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 t);
         assert false
   and aux_attributes xmlattrs mathonly xref  prec t =
     let reset = ref false in
@@ -357,7 +350,7 @@ 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 =
     let attrs = make_href xmlattrs xref in
@@ -400,7 +393,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 +401,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? *)