First commit with new (incomplete) disambiguation engine.

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

diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml
index 04440ffe7a75cefe1ce1b7d9315f2ef197928611..305fe57947edba39d50e13c0c834230b1e15a023 100644 (file)
--- a/matitaB/components/content_pres/cicNotationPres.ml
+++ b/matitaB/components/content_pres/cicNotationPres.ml
@@ -262,32 +262,12 @@ let render status ~lookup_uri ?(prec=(-1)) =
           @ make_href xmlattrs xref
         in
         Mpres.Mo (attrs, to_unicode literal)
-    | A.Ident (literal, subst)
-    | A.Uri (literal, subst) ->
+    | A.Ident (literal, _) ->
         let attrs =
           (RenderingAttrs.ident_attributes `MathML)
           @ make_href xmlattrs xref
         in
-        let name = Mpres.Mi (attrs, to_unicode literal) in
-        (match subst with
-        | Some []
-        | None -> name
-        | Some substs ->
-            let substs' =
-              box_of mathonly (A.H, false, false) []
-                (open_brace
-                :: (NotationUtil.dress semicolon
-                    (List.map
-                      (fun (name, t) ->
-                        box_of mathonly (A.H, false, false) [] [
-                          Mpres.Mi ([], name);
-                          Mpres.Mo ([], to_unicode "\\def");
-                          aux [] mathonly xref  prec t ])
-                      substs))
-                @ [ closed_brace ])
-            in
-            let substs_maction = toggle_action [ hidden_substs; substs' ] in
-            box_of mathonly (A.H, false, false) [] [ name; substs_maction ])
+        Mpres.Mi (attrs, to_unicode literal)
     | A.Meta(n, l) ->
         let local_context l =
           box_of mathonly (A.H, false, false) []